Library hanoi.shanoi4

From mathcomp Require Import all_ssreflect finmap.
From hanoi Require Import extra star gdist lhanoi3 ghanoi ghanoi4 shanoi.


Open Scope nat_scope.


Set Implicit Arguments.

Unset Strict Implicit.



Section sHanoi4.


Local Notation "c1 `-->_s c2" := (smove c1 c2)
    (format "c1 `-->_s c2", at level 60).

Local Notation "c1 `-->*_s c2" := (connect smove c1 c2)
    (format "c1 `-->*_s c2", at level 60).


Let p0 : peg 4 := ord0.


Lemma pE4 (p1 p2 p3 : peg 4) p :
   p1 != p2 p1 != p3 p2 != p3
   p1 != p0 p2 != p0 p3 != p0
  [\/ p = p0, p = p1, p = p2 | p = p3].

Proof.

rewrite /p0.

by case: (peg4E p1) ⇒ ->; rewrite ?eqxx //;
   case: (peg4E p2) ⇒ ->; rewrite ?eqxx //;
   case: (peg4E p3) ⇒ ->; rewrite ?eqxx //;
   case: (peg4E p) ⇒ ->; rewrite ?eqxx // ⇒ *;
   try ((by apply: Or41) || (by apply: Or42) ||
        (by apply: Or43) || (by apply: Or44)).

Qed.



Section lift.


Variable p1 p2 p3 : peg 4.


Hypothesis p1Dp0 : p1 != p0.

Hypothesis p2Dp0 : p2 != p0.

Hypothesis p3Dp0 : p3 != p0.

Hypothesis p1Dp2 : p1 != p2.

Hypothesis p1Dp3 : p1 != p3.

Hypothesis p2Dp3 : p2 != p3.


Variable n m : nat.


Definition clmap (c : configuration 3 n) : configuration 4 n :=
 [ffun i
    if c i == 0 :> nat then p1
    else if c i == 1 :> nat then p0 else p2].


Definition clmerge (c : configuration 3 n) : configuration 4 (n + m) :=
  cmerge (clmap c) `c[p3].


Lemma on_top_clmerge x c : on_top x c on_top (tlshift m x) (clmerge c).

Proof.

move⇒ /on_topP oH; apply/on_topPd.

rewrite !ffunE tsplit_tlshift /=.

case: tsplitPy; rewrite !ffunE ⇒ →.

  case: (_ == _) ⇒ [/eqP|]; first by rewrite (negPf p1Dp3).

  case: (_ == _) ⇒ /eqP; first by rewrite eq_sym (negPf p3Dp0).

  by rewrite (negPf p2Dp3).

case: eqP ⇒ [cxE0|cxD0].

  case: eqP ⇒ [cyE0 _| _].

    by rewrite leq_add2r oH //; apply: val_inj; rewrite /= cyE0.

  by case: (_ == _) ⇒ /eqP; rewrite (negPf p1Dp0, negPf p1Dp2).

case: eqP ⇒ [cxE1|cxD1].

  case: (_ == _) ⇒ [/eqP|]; first by rewrite eq_sym (negPf p1Dp0).

  case: eqP ⇒ [cyE1 _|_ /eqP].

    by rewrite leq_add2r oH //; apply: val_inj; rewrite /= cyE1.

  by rewrite eq_sym (negPf p2Dp0).

have cxE2 : c x = 2 :> nat by case: (c x) cxD0 cxD1 ⇒ [] [|[|[]]].

case: eqP ⇒ [_ /eqP|cyD0].

  by rewrite eq_sym (negPf p1Dp2).

case: eqP ⇒ [_ /eqP|cyD1 _].

  by rewrite (negPf p2Dp0).

have cyE2 : c y = 2 :> nat by case: (c y) cyD0 cyD1 ⇒ [] [|[|[]]].

by rewrite leq_add2r oH //; apply: val_inj; rewrite /= cyE2.

Qed.


Lemma move_clmerge c1 c2 : lmove c1 c2 clmerge c1 `-->_s clmerge c2.

Proof.

move⇒ /moveP [d1 [H1d1 H2d1 H3d1 H4d1]].

apply/moveP; (tlshift m d1); split ⇒ //.

- move: H1d1; rewrite !ffunE tsplit_tlshift !ffunE.

  rewrite /lrel /= /srel /ghanoi.srel /=.

  case: (c1 d1) ⇒ [] [|[|[|]]] //=.

  - case: (c2 d1) ⇒ [] [|[|[|]]] //=.

    by rewrite p1Dp0 muln0.

  - case: (c2 d1) ⇒ [] [|[|[|]]] //= _ _ _.

      by rewrite eq_sym p1Dp0.

    by rewrite eq_sym p2Dp0.

  case: (c2 d1) ⇒ [] [|[|[|]]] //= _ _ _.

  by rewrite p2Dp0 muln0.

- moved2; rewrite !ffunE; case: tsplitPj; rewrite !ffunE //.

  moved2E /eqP/val_eqP.

  rewrite /= d2E eqn_add2rH.

  by rewrite (@H2d1 j).

- by apply: on_top_clmerge.

by apply: on_top_clmerge.

Qed.


Lemma path_clmerge c cs :
  path (move (@lrel 3)) c cs
  path smove (clmerge c) [seq clmerge c | c <- cs].

Proof.

elim: cs c ⇒ //= c1 cs IH c2 /andP[mH pH].

by rewrite move_clmerge // IH.

Qed.


Lemma gdist_clmerge c1 c2 :
  `d[clmerge c1, clmerge c2]_smove `d[c1, c2]_(move (@lrel 3)).

Proof.

have /gpath_connect[pa1 pa1H] := move_lconnect3 c1 c2.

rewrite (gpath_dist pa1H) -(size_map clmerge).

apply: gdist_path_le; first by rewrite path_clmerge // (gpath_path pa1H).

by rewrite [LHS]last_map (gpath_last pa1H).

Qed.


End lift.



Lemma leq_shanoi4 p1 p2 n :
   p1 != p0 p2 != p0 p1 != p2
   `d[`c[p1, n],`c[p2, n]]_smove (S_[1] n).*2.

Proof.

elim/ltn_ind : n p1 p2 ⇒ [] [|n] IH p1 p2 p1Dp0 p2Dp0 p1Dp2.

  rewrite alphaS_small double0.

  rewrite (_ : `c[p1] = `c[p2]) ?gdist0 //.

  by apply/ffunP⇒ [] [].

rewrite S1E S1_bigmin -muln2 -bigminMr.

apply/bigmin_leqPi iLn.

have iLn1 : i n.+1 by apply: leq_trans iLn _.

rewrite -{-5}(subnK iLn1).

rewrite eq_sym in p2Dp0.

have [p3 [[p3Dp2 p3Dp0 p3Dp1] _]] := peg4comp3 p1Dp0 p1Dp2 p2Dp0.

rewrite eq_sym in p2Dp0.

pose p1n := `c[p1, n.+1 - i].

pose p2n := `c[p2, n.+1 - i].

pose p3n := `c[p3, n.+1 - i].

pose p1i := `c[p1, i].

pose p2i := `c[p2, i].

pose p3i := `c[p3, i].

pose c1 := cmerge p1n p1i.

pose c2 := cmerge p1n p3i.

pose c3 := cmerge p2n p3i.

pose c4 := cmerge p2n p2i.

have <- : c1 = `c[p1].

  apply/ffunPj; rewrite /c1 !ffunE.

  by case: tsplitPk; rewrite !ffunE.

have <- : c4 = `c[p2].

  apply/ffunPj; rewrite /c1 !ffunE.

  by case: tsplitPk; rewrite !ffunE.

apply: leq_trans
   (_ : _ `d[c1, c2]_smove + `d[c2, c3]_smove + `d[c3, c4]_smove) _.

  apply: leq_trans (leq_add (gdist_triangular _ _ _ _) (leqnn _)).

  apply: gdist_triangular.

rewrite -addnn !mulnDl [X in _ X]addnAC !muln2.

repeat apply: leq_add; first 2 last.

- apply: leq_trans (gdist_merger _ _ _) _; first by apply: sirr.

    by apply: shanoi_connect.

  by rewrite -S1E; apply: IH.

- apply: leq_trans (gdist_merger _ _ _) _; first by apply: sirr.

    by apply: shanoi_connect.

  by rewrite -S1E; apply: IH ⇒ //; rewrite eq_sym.

rewrite div2K; last first.

  rewrite -subn1 oddB ?expn_gt0 // addbT.

  by rewrite odd_exp orbT.

have → : c2 = clmerge p1 p2 p3 _ `c[ord0].

  apply/ffunPx; rewrite !ffunE.

  by case: tsplitP ⇒ // j; rewrite !ffunE /=.

have → : c3 = clmerge p1 p2 p3 _ `c[inord 2].

  apply/ffunPx; rewrite !ffunE.

  by case: tsplitP ⇒ // j; rewrite !ffunE /= inordK.

apply: leq_trans (gdist_clmerge _ _ _ _ _ _ _ _ _) _ ⇒ //;
  try by rewrite eq_sym.

rewrite gdist_lhanoi3p /lrel /= inordK //=.

case: eqP⇒ [/val_eqP/=|]; first by rewrite inordK.

by rewrite muln1.

Qed.


Fixpoint distanceL n (l : seq (configuration 4 n)) : nat :=
  if l is a :: l1 then
    if l1 is b :: _ then `d[a, b]_smove + distanceL l1
    else 0
  else 0.


Notation " D[ l ] " := (distanceL l)
  (format " D[ l ]").


Definition apeg p1 p2 n : peg 4 := if odd n then p2 else p1.

Notation " a[ p1 , p2 ] " := (apeg p1 p2)
  (format " a[ p1 , p2 ]").


Lemma apeg32E a p1 p2 : a[p1, p2] (3 × a).-2 = a[p1, p2] a.

Proof.

case: a ⇒ // a.

rewrite /apeg -subn2 oddB; last by rewrite mulnS.

by rewrite odd_mul /=; case: odd.

Qed.


Lemma apeg0 p1 p2 : a[p1, p2] 0 = p1.

Proof.
by []. Qed.

Lemma apegS p1 p2 n : a[p1, p2] n.+1 = a[p2, p1] n.

Proof.
by rewrite /apeg /=; case: odd. Qed.

Lemma apegO p1 p2 n : a[p1, p2] n = a[p2, p1] (~~ (odd n)).

Proof.
by rewrite /apeg /=; case: odd. Qed.

Lemma apeg_double p1 p2 n : a[p1, p2] (n.*2) = p1.

Proof.
by rewrite apegO odd_double. Qed.

Lemma apeg_neq p1 p2 p3 n : p1 != p3 p2 != p3 a[p1, p2] n != p3.

Proof.
by rewrite /apeg /=; case: odd; rewrite // eq_sym. Qed.

Lemma apeg_eqC p1 p2 n : (a[p1, p2] n == a[p2, p1] n) = (p1 == p2).

Proof.
by rewrite /apeg /=; case: odd; rewrite // eq_sym. Qed.

Lemma apegD p1 p2 m n : a[p1, p2] (m + n) = a[ a[p1, p2] n, a[p2, p1] n] m.

Proof.
by rewrite /apeg oddD; do 2 case: odd. Qed.

Lemma apegMr p1 p2 m n : odd m a[p1, p2] (m × n) = a[p1, p2] n.

Proof.
by rewrite /apeg; rewrite odd_mul ⇒ →. Qed.

Lemma codom_apeg (A : finType) (f : {ffun A _}) p1 p2 n :
  (codom f \subset [:: a[p1, p2] n; a[p2, p1] n]) =
  (codom f \subset [:: p1; p2]).

Proof.
by rewrite /apeg; case: odd; rewrite // codom_subC. Qed.

Lemma sgdist_pair n (p2 : peg 4) (u v : configuration 4 n.+1)
    (p1 := u ldisk) (p3 := v ldisk):
   {st : (configuration 4 n × configuration 4 n) |
    p1 != p2 p1 != p3 p2 != p3
    p1 != p0 p2 != p0 p3 != p0
     [/\ codom st.1 \subset [:: p2; p3], codom st.2 \subset [:: p1; p2] &
         `d[u, v]_smove = D[[:: ↓[u]; st.1; st.2; ↓[v]]].+2]}.

Proof.

case: eqP ⇒ [_|/eqP p1Dp2]; first by (↓[u], ↓[v]).

case: eqP ⇒ [_|/eqP p1Dp3]; first by (↓[u], ↓[v]).

case: eqP ⇒ [_|/eqP p2Dp3]; first by (↓[u], ↓[v]).

case: eqP ⇒ [_|/eqP p1Dp0]; first by (↓[u], ↓[v]).

case: eqP ⇒ [_|/eqP p2Dp0]; first by (↓[u], ↓[v]).

case: eqP ⇒ [_|/eqP p3Dp0]; first by (↓[u], ↓[v]).

have pE p : [\/ p = p0, p = p1, p = p2 | p = p3] by apply: pE4.

have [cs /= csH] := gpath_connect (shanoi_connect u v).

have vIcs : v \in cs.

  have := mem_last u cs; rewrite (gpath_last csH).

  rewrite inE; case: eqP ⇒ // vEu.

  by case/eqP : p1Dp3; rewrite /p3 vEu.

case: (@split_first _ cs (fun cc ldisk != p1)) ⇒ [|[[sp cs1] cs2]].

  apply/negP⇒ /allP /(_ _ vIcs).

  rewrite /= -topredE /= negbK.

  by rewrite eq_sym (negPf p1Dp3).

case⇒ /allP spH spLE csE.

pose s := last u cs1.

have sMsp : s `-->_s sp.

  by have := gpath_path csH; rewrite csE cat_path ⇒ /and3P[].

have sLp1 : s ldisk = p1.

  move: (spH s); rewrite /s; case: (cs1) ⇒ //= c cs3 /(_ (mem_last _ _)).

  by rewrite -topredE negbK ⇒ /eqP.

have spLp0 : sp ldisk = p0.

  apply/eqP.

  have /(_ ldisk) := move_diskr sMsp.

  rewrite eq_sym sLp1 ⇒ /(_ spLE) /andP[].

  case: (_ =P p0) ⇒ // /val_eqP /=.

  have /eqP/val_eqP/= := p1Dp0.

  by case: (p1 : nat) ⇒ // k; case: (sp _ : nat).

have sCd : codom (↓[s]) \subset [:: p2; p3].

  apply/subsetPi; rewrite !inE ⇒ /codomP[j] →.

  case: (pE (↓[s] j)) ⇒ [||->|->]; rewrite ?eqxx ?orbT //.

    rewrite ffunE trshift_lift /=.

    move/eqP; rewrite -spLp0 -[_ == _]negbK; case/negP.

    apply: move_on_toplDr sMsp _ _; first by rewrite sLp1 spLp0.

    by rewrite /= /bump [n j]leqNgt ltn_ord add0n ltnW.

  rewrite ffunE trshift_lift /=.

  move/eqP; rewrite -sLp1 -[_ == _]negbK; case/negP.

  apply: move_on_toplDl sMsp _ _; first by rewrite sLp1 spLp0.

  by rewrite /= /bump [n j]leqNgt ltn_ord add0n.

have vIcs2 : v \in cs2.

  move: vIcs; rewrite csE !(inE, mem_cat) ⇒ /or3P[|/eqP vEs|] //.

    by move⇒ /spH; rewrite /= -topredE negbK eq_sym (negPf p1Dp3).

  by case/eqP : p3Dp0; rewrite /p3 vEs.

case: (@split_last _ (sp :: cs2) (fun cc ldisk != p3)) ⇒
     [|/= [[t cs3] cs4]/=].

  apply/negP⇒ /allP /(_ _ (mem_head _ _)).

  by rewrite /= -topredE /= negbK spLp0 eq_sym (negPf p3Dp0).

case⇒ // tLE tH scs2E.

have vIcs4 : v \in cs4.

  have := gpath_last csH; rewrite csE scs2E !last_cat /=.

  case: (cs4) ⇒ /= [tEv|c1 cs5 <-]; last by apply: mem_last.

  by case/eqP: tLE; rewrite tEv.

  case: cs4 tH scs2E vIcs4 ⇒ // tp cs4 /allP tH scs2E vItpcs4.

have tMtp : t `-->_s tp.

  by have := gpath_path csH; rewrite csE scs2E !cat_path /= ⇒ /and5P[].

have tpLp3 : tp ldisk = p3.

  by move: (tH _ (mem_head _ _)); rewrite /= -topredE negbK ⇒ /eqP.

have tLp0 : t ldisk = p0.

  apply/eqP.

  have /(_ ldisk) := move_diskr tMtp.

  rewrite tpLp3 ⇒ /(_ tLE) /andP[].

  case: (_ =P p0) ⇒ // /val_eqP /=.

  have /eqP/val_eqP/= := p3Dp0.

  by case: (p3 : nat) ⇒ // k; case: (t _ : nat).

have tCd : codom (↓[t]) \subset [:: p1; p2].

  apply/subsetPi; rewrite !inE ⇒ /codomP[j] →.

  case: (pE (↓[t] j)) ⇒ [|->|->|]; rewrite ?eqxx ?orbT //.

    rewrite ffunE trshift_lift /=.

    move/eqP; rewrite -tLp0 -[_ == _]negbK; case/negP.

    apply: move_on_toplDl tMtp _ _; first by rewrite tpLp3 tLp0 eq_sym.

    by rewrite /= /bump [n j]leqNgt ltn_ord add0n.

  rewrite ffunE trshift_lift /=.

  move/eqP; rewrite -tpLp3 -[_ == _]negbK; case/negP.

  apply: move_on_toplDr tMtp _ _; first by rewrite tpLp3 tLp0 eq_sym.

  by rewrite /= /bump [n j]leqNgt ltn_ord add0n ltnW.

(↓[s], ↓[t]); split ⇒ //=.

rewrite addn0.

move: csH; rewrite csEcsH.

rewrite (gdist_cat csH) -/s.

move: csH ⇒ /gpath_catr; rewrite -/scsH.

rewrite gdist_cunlift_eq //; try apply: sirr; last by apply: shanoi_connect.

rewrite -!addnS.

congr (_ + _).

have ->: ↓[s] = ↓[sp].

  have sLDspL : s ldisk != sp ldisk by rewrite sLp1 spLp0.

  apply/ffunPi; rewrite !ffunE.

  apply: move_disk1 sMsp sLDspL _.

  by apply/negP ⇒ /eqP/val_eqP /=; rewrite eqn_leq leqNgt ltn_ord.

rewrite (gdist_cons csH) addnS; congr (_).+1.

move: csH ⇒ /gpath_consr csH.

have ctEctp : ↓[t] = ↓[tp].

  have tLDtpL : t ldisk != tp ldisk by rewrite tLp0 tpLp3 eq_sym.

  apply/ffunPi; rewrite !ffunE.

  apply: move_disk1 tMtp tLDtpL _.

  by apply/negP ⇒ /eqP/val_eqP /=; rewrite eqn_leq leqNgt ltn_ord.

case: cs3 scs2E ⇒ [[spEt cs2E]|c3 cs3 /= [spE cs2E]].

  move: csH; rewrite spEt cs2EcsH.

  rewrite gdist0 add0n (gdist_cons csH) ctEctp.

  move: csH ⇒ /gpath_consr csH.

  rewrite gdist_cunlift_eq //; try by apply: sirr.

  by apply: shanoi_connect.

move: csH; rewrite cs2E -cat_rconscsH.

rewrite (gdist_cat csH) last_rcons.

rewrite gdist_cunlift_eq //; try apply: sirr; last 2 first.

- by apply: shanoi_connect.

- by rewrite tLp0.

congr (_ + _).

move: csH ⇒ /gpath_catr; rewrite last_rconscsH.

rewrite (gdist_cons csH); congr (_).+1.

move: csH ⇒ /gpath_consr csH.

rewrite ctEctp gdist_cunlift_eq //; try apply: sirr.

by apply: shanoi_connect.

Qed.


Definition sgdist1 n (p2 : peg 4) (u v : configuration 4 n.+1) :=
 let: (exist (x, _) _) := sgdist_pair p2 u v in x.


Definition sgdist2 n (p2 : peg 4) (u v : configuration 4 n.+1) :=
 let: (exist (_, x) _) := sgdist_pair p2 u v in x.


Lemma sgdistE n (p2 : peg 4) (u v : configuration 4 n.+1)
    (p1 := u ldisk) (p3 := v ldisk):
    p1 != p2 p1 != p3 p2 != p3
    p1 != p0 p2 != p0 p3 != p0
   [/\ codom (sgdist1 p2 u v) \subset [:: p2; p3],
       codom (sgdist2 p2 u v) \subset [:: p1; p2] &
       `d[u, v]_smove = D[[:: ↓[u]; sgdist1 p2 u v; sgdist2 p2 u v; ↓[v]]].+2].

Proof.

movep1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0.

by rewrite /sgdist1 /sgdist2; case: sgdist_pair ⇒ [] [x y] [].

Qed.


Definition beta n l k :=
  if ((1 < l) && (k == n.-1)) then α_[l] k else (α_[1] k).*2.


Local Notation "β_[ n , l ]" := (beta n l) (format "β_[ n , l ]" ).


Lemma leq_beta n l k : α_[l] k β_[n, l] k.

Proof.

rewrite /beta; case: (_ < _) ⇒ /=; last first.

  by apply: bound_alphaL.

by case: (_ == _) ⇒ //=; apply: bound_alphaL.

Qed.


Lemma geq_beta n l k : β_[n, l] k (α_[1] k).*2.

Proof.

rewrite /beta; case: (_ < _) ⇒ //=.

by case: (_ == _) ⇒ //=; apply: bound_alphaL.

Qed.


Lemma beta1E n k : β_[n, 1] k = (α_[1] k).*2.

Proof.
by rewrite /beta ltnn. Qed.

Definition sp n (a : configuration 4 n) l p :=
  \sum_(k < n) (a k != p) × β_[n, l] k.


Lemma sum_beta_S n l (a : configuration 4 n.+1) p : 1 < l
  sp a l p =
  \sum_(k < n) ((↓[a] k != p) × (α_[1] k).*2) + (a ord_max != p) × α_[l] n.

Proof.

movel_gt1; rewrite /sp.

rewrite big_ord_recr /= /beta l_gt1 eqxx /=; congr (_ + _).

apply: eq_bigri _; rewrite !ffunE; congr ((a _ != _) × _).

  by apply: val_inj.

by rewrite eqn_leq [_ i]leqNgt ltn_ord andbF.

Qed.


Lemma leq_sum_beta n l a :
  \sum_(k < n) a k × β_[n, l] k \sum_(k < n) a k × (α_[1] k).*2.

Proof.

by apply: leq_sumi _; rewrite leq_mul2l geq_beta orbT.

Qed.


Lemma sum_alpha_diffE n (f : configuration 4 n.+1) (p1 p2 : peg 4) v1 v2 :
  1 < v1 1 < v2 p1 != p2 codom f \subset [:: p1; p2]
  sp f v1 p1 + sp f v2 p2 (S_[1] n).*2 + α_[maxn v1 v2] n.

Proof.

movev1_gt1 v2_gt1 p1Dp2 cH.

rewrite !sum_beta_S //.

rewrite -addnA -addnCA addnC !addnA -addnA leq_add //.

  rewrite leq_eqVlt; apply/orP; left; apply/eqP.

  rewrite -addnn !dsum_alphaLE -!big_split /=; apply: eq_bigri _.

  rewrite !ffunE; set v := trshift _ _.

  have /subsetP := cH ⇒ /(_ (f v) (codom_f _ _)).

  rewrite !inE addnn.

  case: eqP ⇒ /= x1; case: eqP ⇒ /= x2; rewrite ?(mul1n, add0n, addn0) //.

  by move/eqP: x2; rewrite x1 (negPf p1Dp2).

  have /subsetP/(_ (f ord_max) (codom_f _ _)) := cH.

rewrite !inE.

case: eqP ⇒ /= x1; case: eqP ⇒ /= x2 // _; rewrite ?(mul1n, add0n, addn0) //;
     apply: (increasingE (increasing_alphaL_l _)).

  by apply: leq_maxr.

by apply: leq_maxl.

Qed.


Section Case1.


Definition sd n l (u : {ffun 'I_l.+1 configuration 4 n}) :=
    \sum_(i < l) `d[u (inord i), u (inord i.+1)]_smove.


Variable n : nat.

Hypothesis IH:
      (l : nat) (p1 p2 p3 : ordinal_eqType 4)
       (u : {ffun 'I_l.+1 configuration 4 n.+1}),
     p1 != p2
     p1 != p3
     p2 != p3
     p1 != p0
     p2 != p0
     p3 != p0
     ( k : 'I_l.+1,
      0 < k < l codom (u k) \subset [:: p2; a[p1, p3] k])
     (S_[l] n.+1).*2 sd u +
                     sp (u ord0) l (a[p1, p3] 0) +
                     sp (u ord_max) l (a[p1, p3] l).


Variable l : nat.

Variables p1 p2 p3: peg 4.

Variable u : {ffun 'I_l.+2 configuration 4 n.+2}.

Hypothesis p1Dp2 : p1 != p2.

Hypothesis p1Dp3 : p1 != p3.

Hypothesis p2Dp3 : p2 != p3.

Hypothesis p1Dp0 : p1 != p0.

Hypothesis p2Dp0 : p2 != p0.

Hypothesis p3Dp0 : p3 != p0.

Hypothesis cH : k : 'I_l.+2,
     0 < k < l.+1 codom (u k) \subset [:: p2; a[p1, p3] k].


Let u':= ([ffun i ↓[u i]] : {ffun 'I_l.+2 configuration 4 n.+1})
 : {ffun 'I_l.+2 configuration 4 n.+1}.


Let H: k : 'I_l.+2,
    0 < k < l.+1 codom (u' k) \subset [:: p2; a[p1, p3] k].

Proof.
by movek kH; rewrite ffunE; apply/codom_liftr/cH. Qed.

Let apeg13D2 a : a[p1, p3] a != p2.

Proof.
by rewrite /apeg; case: odd; rewrite // eq_sym. Qed.

Let apeg13D0 a : a[p1, p3] a != p0.

Proof.
by rewrite /apeg; case: odd; rewrite // eq_sym. Qed.

Hypothesis KH1 : u ord0 ord_max = p1.

Hypothesis KH2 : u ord_max ord_max != a[p3, p1] l.

Hypothesis l_gt0 : l != 0.


Lemma case1 :
  (S_[l.+1] n.+2).*2
  sd u + sp (u ord0) l.+1 p1 +
         sp (u ord_max) l.+1 (a[p3, p1] l).

Proof.

have il1E : inord l.+1 = ord_max :> 'I_l.+2
  by apply/val_eqP; rewrite /= inordK.

have iE : i, u (inord i) ord_max != a[p1, p3] i.

  by l.+1; rewrite apegS il1E.

case: (@ex_minnP _ iE) ⇒ a aH aMin.

have aMin1 i : i < a u (inord i) ord_max = a[p1, p3] i.

  by case: (u (inord i) ord_max =P a[p1, p3] i) ⇒ // /eqP /aMin; case: leqP.

have aLld1 : a l.+1 by apply: aMin; rewrite apegS il1E.

have a_gt0 : 0 < a by case: (a) aH; rewrite // apeg0 -KH1 inord_eq0 //= eqxx.

pose ai : 'I_l.+2 := inord a.

have aiE : ai = a :> nat by rewrite inordK.

pose b := l.+1 - a.

pose bi : 'I_l.+2 := inord b.

have biE : bi = b :> nat by rewrite inordK // /b ltn_subLR // leq_addl.

have l_ggt0 : 0 < l by case: l l_gt0.

have [/andP[a_gt1 aLlm1]|] := boolP (2 a l.-1).

  have aLl : a l by rewrite (leq_trans aLlm1) // -subn1 leq_subr.

  have b_gt1 : 1 < b by rewrite leq_subRL // addn2 ltnS -[l]prednK.

  have uaiLEp2 : u ai ldisk = p2.

    have /cH/subsetP/(_ (u ai ldisk) (codom_f _ _)) : 0 < ai < l.+1.

      by rewrite aiE (leq_trans _ a_gt1) //= ltnS (leq_trans aLl1)
                 // ssrnat.leq_pred.

    by rewrite !inE aiE (negPf aH) orbF ⇒ /eqP.

  pose si i : configuration 4 n.+1 :=
     sgdist1 p2 (u (inord i)) (u (inord i.+1)).

  pose ti i : configuration 4 n.+1 :=
     sgdist2 p2 (u (inord i)) (u (inord i.+1)).

  have sitiH i : i < a.-1
     [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
         codom (ti i) \subset [:: u (inord i) ldisk; p2] &
         `d[u (inord i), u (inord i.+1)]_smove =
           D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].

    moveiLa.

    have iLa1 : i < a by rewrite (leq_trans iLa) // ssrnat.leq_pred.

    apply: sgdistE ⇒ //.

    - by rewrite aMin1.

    - rewrite !aMin1 //; last by rewrite -[a]prednK.

      by rewrite apegS apeg_eqC.

    - by rewrite aMin1 1?eq_sym // -[a]prednK.

    - by rewrite aMin1.

    by rewrite aMin1 // -[a]prednK.

  pose sam1 : configuration 4 n.+1 :=
     sgdist1 (a[p1, p3] a) (u (inord a.-1)) (u (inord a)).

  pose tam1 : configuration 4 n.+1 :=
     sgdist2 (a[p1, p3] a) (u (inord a.-1)) (u (inord a)).

  have [sam1C tam1C duam1ua1E] :
     [/\ codom sam1 \subset [:: a[p1, p3] a; u (inord a) ldisk ],
         codom tam1 \subset [:: u (inord a.-1) ldisk; a[p1, p3] a] &
         `d[u (inord a.-1), u (inord a)]_smove =
           D[[:: ↓[u (inord a.-1)]; sam1; tam1; ↓[u (inord a)]]].+2].

    apply: sgdistE ⇒ //.

    - by rewrite aMin1 ?prednK // -{2}[a]prednK //= apegS apeg_eqC.

    - by rewrite uaiLEp2 aMin1 ?prednK.

    - by rewrite uaiLEp2.

    - by rewrite aMin1 ?prednK.

    by rewrite uaiLEp2.

  have {}tam1C : codom tam1 \subset [:: p1; p3].

    move: tam1C; rewrite aMin1; last by rewrite -{2}[a]prednK.

    rewrite -subn1 apegO oddB //= [a[_, _]a]apegO; case: odd ⇒ //=.

    by rewrite codom_subC.

  pose u1 :=
    [ffun i
    if ((i : 'I_(3 × a).-2.+1) == 3 × a.-1 :>nat) then ↓[u (inord a.-1)]
    else if (i == (3 × a.-1).+1 :>nat) then sam1
    else if (i %% 3) == 0 then ↓[u (inord (i %/ 3))]
    else if (i %% 3) == 1 then si (i %/ 3)
    else ti (i %/ 3)].

  have u10E : u1 ord0 = ↓[u ord0].

    rewrite ffunE /= ifN ?inord_eq0 //.

    by rewrite neq_ltn muln_gt0 /= -ltnS prednK //= a_gt1.

  have uiME : u1 ord_max = sam1.

    rewrite ffunE /= eqn_leq leqNgt -{2}[a]prednK // mulnS.

    rewrite addSn add2n ltnS leqnn /=.

    by rewrite -{1}[a]prednK // mulnS eqxx.

  pose u2 := [ffun i : 'I_3
    if i == 0 :> nat then sam1 else
    if i == 1 :> nat then tam1 else ↓[u ai]].

  pose u3 := [ffun i ↓[u (inord ((i : 'I_b.+1) + a))]].

  have P1 : a.*2 + sd u1 + sd u2 + sd u3 sd u.

    have G b1 : b1 = a
      \sum_(i < (3 × b1).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove =
      \sum_(i < (3 × a.-1)) `d[u1 (inord i), u1 (inord i.+1)]_smove +
      `d[↓[u (inord a.-1)], sam1]_smove.

      moveb1Ea.

      have ta2E : (3 × b1).-2 = (3 × a.-1).+1.

        by rewrite b1Ea -{1}[a]prednK // mulnS.

      rewrite ta2E big_ord_recr /=; congr (_ + `d[_,_]_smove).

        by rewrite ffunE ifT// inordK // -{2}b1Ea ?ta2E.

      rewrite ffunE inordK; last by rewrite -{2}b1Ea ?ta2E.

      by rewrite eqn_leq ltnn /= eqxx.

    rewrite {}[sd u1]G //.

    have → := @sum3E _ (fun i`d[u1 (inord i), u1 (inord i.+1)]_smove).

    have → : a.*2 = 2 + \sum_(i < a.-1) 2.

      rewrite sum_nat_const /= cardT size_enum_ord.

      by rewrite muln2 -(doubleD 1) add1n prednK.

    rewrite !addnA -[2 + _ + _]addnA -big_split /=.

    rewrite [2 + _]addnC -!addnA 2![X in _ + X _]addnA addnA.

    have → : sd u =
      \sum_(i < a.-1) (`d[u (inord i), u (inord i.+1)]_smove) +
      `d[u (inord a.-1), u ai]_smove +
      \sum_(i < b) `d[u (inord (a +i)), u (inord (a + i.+1))]_smove.

      have F := big_mkord xpredT
                    (fun i`d[u (inord i), u (inord i.+1)]_smove).

      rewrite -{}[sd u]F.

      rewrite (big_cat_nat _ _ _ (_ : _ (a.-1).+1)) //=; last first.

         by rewrite prednK.

      rewrite big_mkord big_ord_recr /= prednK //.

      rewrite -{9}[a]add0n big_addn -/b big_mkord.

      congr (_ + _ + _).

      by apply: eq_bigri; rewrite addnC addnS.

    apply: leq_add; first apply: leq_add.

    - rewrite leq_eqVlt; apply/orP; left; apply/eqP.

      apply: eq_bigri _.

      have → : u1 (inord (3 × i)) = ↓[u (inord i)].

        rewrite ffunE inordK; last first.

          rewrite ltnS (leq_trans (_ : _ 3 × (a.-1))) //.

            by rewrite leq_mul2l /= ltnW.

          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.

        rewrite eqn_mul2l /= eqn_leq [_ i]leqNgt ltn_ord andbF.

        rewrite eqn_leq ltn_mul2l /= ltnNge [i _]ltnW // andbF.

        by rewrite mod3E eqxx mulKn.

      have → : u1 (inord (3 × i).+1) = si i.

        rewrite ffunE inordK; last first.

          rewrite ltnS (leq_trans (_ : _ 3 × (a.-1))) //.

            by rewrite ltn_mul2l /=.

          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.

        rewrite eqn_leq [_ _.+1]leqNgt.

        rewrite (leq_trans (_ : (3 × i).+2 (3 × i.+1))) ?andbF //;
               last 2 first.

        - by rewrite mulnS addSn add2n.

        - by rewrite leq_mul2l /=.

        rewrite eqn_leq !ltnS [_ 3 × i]leq_mul2l.

        by rewrite [_ i]leqNgt ltn_ord andbF mod3E /= div3E.

      have → : u1 (inord (3 × i).+2) = ti i.

        rewrite ffunE inordK; last first.

          rewrite ltnS (leq_trans (_ : _ 3 × (a.-1))) //.

            rewrite (leq_trans (_ : _ 3 × (i.+1))) //.

              by rewrite mulnS addSn add2n.

            by rewrite leq_mul2l /=.

          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.

        rewrite eqn_leq [_ _.+1]leqNgt.

        rewrite -[(3 × i).+3](mulnDr 3 1 i) leq_mul2l ltn_ord andbF.

        rewrite eqn_leq !ltnS [_ _.+1]leqNgt.

        rewrite (leq_trans (_ : (3 × i).+1 < 3 × (i.+1))) ?andbF //;
             last 2 first.

        - by rewrite mulnS addSn add2n.

        - by rewrite leq_mul2l /=.

        by rewrite mod3E /= div3E.

      have → : u1 (inord (3 × i).+3) = ↓[u (inord i.+1)].

        have → : (3 × i).+3 = 3 × (i.+1) by rewrite mulnS addSn add2n.

        rewrite ffunE inordK; last first.

          rewrite ltnS (leq_trans (_ : _ 3 × (a.-1))) //.

            by rewrite leq_mul2l /=.

          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.

        rewrite eqn_mul2l /=; case: eqP ⇒ [->//|_].

        rewrite eqn_leq [_ 3 × i.+1]leqNgt ltnS leq_mul2l /= ltn_ord andbF.

        by rewrite mod3E /= div3E.

      case: (sitiH i) ⇒ // _ _ →.

      by rewrite add2n /= addnA addn0.

    - rewrite leq_eqVlt; apply/orP; left; apply/eqP.

      rewrite /sd !big_ord_recr big_ord0 //= add0n !addnA.

      have → : u2 (inord 0) = sam1 by rewrite ffunE /= inordK.

      have → : u2 (inord 1) = tam1 by rewrite ffunE /= inordK.

      have → : u2 (inord 2) = ↓[u ai] by rewrite ffunE /= inordK.

      by move: duam1ua1E; rewrite /= addn0 add2n !addnA !addSn.

    apply: leq_sumi _.

    rewrite ffunE inordK; last by rewrite ltnS ltnW.

    rewrite ffunE inordK; last by rewrite ltnS.

    rewrite addSn [i + _]addnC addnS.

    by apply/gdist_cunlift/shanoi_connect.

  set x1P1 := sd _ in P1; set x2P1 := sd _ in P1.

  set x3P1 := sd _ in P1; set xP1 := sd _ in P1.

  rewrite -/xP1.

  have cH2 (k : 'I_(3 × a).-2.+1) :
      0 < k < (3 × a).-2 codom (u1 k) \subset [:: p2; a[p1, p3] k].

    move⇒ /andP[k_gt0 k_lt].

    have kL3a1 : k (3 × a.-1).

      by rewrite -ltnS (leq_trans k_lt) // -{1}[a]prednK // mulnS.

    have kLa1 : k %/ 3 a.-1.

      by rewrite -(mulKn a.-1 (isT : 0 < 3)) leq_div2r.

    rewrite ffunE; case: eqP ⇒ [kH|/eqP kH].

      rewrite kH apegMr //.

      have := @H (inord a.-1); rewrite inordK //.

        rewrite ffunE; apply.

        by rewrite -ltnS prednK // a_gt1.

      by rewrite prednK // (leq_trans aLld1).

    have k3La2 : k %/ 3 a.-2.

      rewrite -ltnS [a.-2.+1]prednK //; last first.

        by rewrite -subn1 ltn_subRL.

      rewrite ltn_divLR // [_ × 3]mulnC.

      by move: kL3a1 kH; case: ltngtP.

    rewrite eqn_leq [_ k]leqNgt (leq_trans k_lt) ?andbF //; last first.

      by rewrite -{1}[a]prednK // mulnS addSn add2n.

    have k3La : k %/ 3 a.

      by rewrite (leq_trans kLa1) // -subn1 leq_subr.

    case: eqPk3mH.

      apply: codom_liftr.

      rewrite {2}(divn_eq k 3) k3mH addn0 [in a[_,_] _]mulnC apegMr //.

      have := @cH (inord (k %/3)); rewrite inordK; last first.

        by rewrite (leq_ltn_trans k3La).

      apply.

      rewrite (leq_ltn_trans k3La) ?ltnS //.

      move: k_gt0; rewrite andbT {1}(divn_eq k 3) k3mH addn0 muln_gt0.

      by case/andP.

    case: eqPk3mH1.

      case: (sitiH ((k %/ 3))) ⇒ /=.

        by rewrite -[a.-1]prednK // -ltnS prednK.

      set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp.

      set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k.

        rewrite (divn_eq k 3) k3mH1 addn1 apegS mulnC apegMr //.

        by rewrite /i !inordK ?apegS //= !ltnS (leq_trans k3La).

      have H2 : (k %/ 3).+1 < l.+2 by rewrite !ltnS (leq_trans k3La).

      rewrite -(@aMin1 i); last first.

        rewrite !inordK // -{2}[a]prednK // ltnS // -[a.-1]prednK // .

        by rewrite -subn1 subn_gt0.

      congr (u _ _).

      by apply/val_eqP; rewrite /= !inordK.

    rewrite codom_subC.

    case: (sitiH ((k %/ 3))) ⇒ /= [|_].

      by rewrite -[a.-1]prednK // -ltnS prednK.

    set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp.

    set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k.

      have k3mH2 : k %% 3 = 2.

        have := ltn_mod k 3; move: k3mH k3mH1.

        by case: modn ⇒ // [] [|[]].

      rewrite (divn_eq k 3) k3mH2 addn2 !apegS mulnC apegMr //.

        by rewrite /i !inordK ?apegS //= !ltnS (leq_trans k3La).

      have H2 : (k %/ 3) < l.+2 by rewrite !ltnS (leq_trans k3La).

      rewrite -(@aMin1 i); last by rewrite !inordK // -{2}[a]prednK .

      congr (u _ _).

      by apply/val_eqP; rewrite /= !inordK.

  have {cH2}P2 := IH p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 cH2.

  have a3B2_gt1 : 1 < (3 × a).-2.

    rewrite -subn2 leq_subRL.

      by rewrite (leq_trans (_ : 4 3 × 2)) // leq_mul2l.

    by rewrite (leq_trans (_ : 2 3 × 2)) // leq_mul2l.

  rewrite u10E uiME apeg0 in P2.

  have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                          (leqnn _)).

  pose pa := a[p1, p3] a; pose paS := a[p1, p3] a.+1.

  have cH3 (k : 'I_3) :
    0 < k < 2 codom (u2 k) \subset [:: paS; a[p2, pa] k].

    case: k ⇒ [] [|[|]] //= iH _.

    by rewrite /pa /paS !apegS apeg0 ffunE /= codom_apeg codom_subC.

  rewrite -/x1P1 in P2.

  have {cH3}P3 :
    (S_[2] n.+1).*2 sd u2 + sp (u2 ord0) 2 (a[p2, pa] 0) +
                       sp (u2 ord_max) 2 (a[p2, pa] 2).

    apply: IH cH3 ⇒ //; try by rewrite /pa /paS // eq_sym.

    by rewrite /pa /paS apegS apeg_eqC eq_sym.

  rewrite !ffunE /= apeg0 -/x2P1 in P3.

  have cH4 (k : 'I_b.+1) :
      0 < k < b codom (u3 k) \subset [:: p2; a[pa, paS] k].

      rewrite /b .

    move⇒ /andP[k_gt0 kLb].

    have kBound : 0 < k + a < l.+1.

      rewrite (leq_trans a_gt0) ?leq_addl //=.

      by move: kLb; rewrite /b ltn_subRL addnC.

    rewrite ffunE codom_liftr //.

    have := @cH (inord (k + a)).

    rewrite /pa /paS apegS inordK; first by rewrite -apegD; apply.

    by rewrite ltnW // ltnS; case/andP: kBound.

  have {cH4}P4 :
   (S_[b] n.+1).*2 sd u3 + sp (u3 ord0) b (a[pa, paS] 0) +
                      sp (u3 ord_max) b (a[pa, paS] b).

    apply: IH cH4 ⇒ //; try by rewrite /pa /paS // eq_sym.

    by rewrite /pa /paS apegS apeg_eqC.

  have {}P4 := leq_trans P4 (leq_add (leqnn _) (leq_sum_beta _ _)).

  rewrite apeg0 /= (_ : a[_, _] b = a[p3, p1] l) in P4; last first.

    by rewrite /pa /paS apegS -apegD subnK ?apegS.

  rewrite !ffunE /= add0n -/ai in P4.

  rewrite -/x3P1 subnK // (_ : inord l.+1 = ord_max) in P4; last first.

    by apply/val_eqP; rewrite /= inordK.

  rewrite [X in _ _ + X + _]sum_beta_S //= KH1 eqxx addn0.

  set xS := \sum_(_ < _) _ in P2; rewrite -/xS.

  rewrite [X in _ _ + _ + X]sum_beta_S //= KH2 mul1n.

  set yS := \sum_(_ < _) _ in P4; rewrite -/yS.

  set x1S := sp _ _ _ in P2; set y1S := sp _ _ _ in P3.

  have x1Sy1SE : x1S + y1S (S_[1] n).*2 + α_[maxn (3 × a).-2 2] n.

    apply: sum_alpha_diffE ⇒ //.

    rewrite apeg32E //.

    by move: sam1C; rewrite -uiME uaiLEp2.

  rewrite (maxn_idPl _) // in x1Sy1SE.

  set x2S := sp _ _ _ in P3; set y2S := sp _ _ _ in P4.

  have x2y2SE : x2S + y2S (S_[1] n).*2 + α_[maxn 2 b] n.

    apply: sum_alpha_diffE ⇒ //; first by rewrite /pa eq_sym.

    have /H : 0 < (inord a : 'I_l.+2) < l.+1 by rewrite inordK // a_gt0.

    by rewrite ffunE inordK.

  rewrite -addnn {1}dsum_alphaL_S in P2.

  rewrite -addnn {1}dsum_alphaL_S in P3.

  rewrite -addnn {1}dsum_alphaL_S.

  have F4 k : S_[a.-1] k.+1 S_[(3 ×a).-2] k + a.-1.

    apply: leq_trans (dsum_alpha3l _ _) _.

    rewrite leq_add2r.

    apply: (increasingE (increasing_dsum_alphaL_l _)).

    by rewrite -{2}[a]prednK // mulnS addSn add2n /=.

  have F4n := F4 n.

  have {F4}F4n1 := F4 n.+1.

  have F5 k :
    S_[l.+1] k.+1 + S_[1] k.+1 + S_[b.+1] k.+1
    S_[a.-1] k.+1 + S_[b.+2] k.+1 + S_[b] k + (α_[1] k).*2.

    have <- : a + b = l.+1 by rewrite addnC subnK.

    rewrite -[X in _ X]addnA (leq_add _ (dsum_alphaL_alpha k b_gt1)) //.

    have := concaveEk1 1 a.-2 b.+1 (concave_dsum_alphaL_l k.+1).

    rewrite add1n prednK; last by rewrite -subn1 ltn_subRL addn0.

    by rewrite -addSnnS prednK // add1n [X in _ X]addnC.

  have F5n := F5 n.

  have {F5}F5n1 := F5 n.+1.

  have F6 k : S_[b.+2] k + S_[1] k S_[b.+1] k + S_[2] k.

    by have := concaveEk1 1 1 b (concave_dsum_alphaL_l k).

  have F6n := F6 n.+1.

  have {F6}F6n1 := F6 n.+2.

  have F72 := dsum_alphaL_S 2 n.+1.

  have F721 := dsum_alphaL_S 2 n.

  have F711 := dsum_alphaL_S 1 n.+1.

  have F71 := dsum_alphaL_S 1 n.

  have F73 := dsum_alphaL_S b n.

  have F8 : α_[2] n.+1 α_[1] n.+2.

    have ->: α_[1] n.+2 = α_[3] n.+1 by rewrite alphaL_3E.

    by apply: increasing_alphaL_l.

  have F9 : α_[1] (n.+2) (α_[1] n).*2.+2.

    apply: leq_trans (leqnSn _).

    by apply: alphaL_4_5.

  gsimpl.

  applyr P1.

  rewrite -(leq_add2r x1S); applyr P2.

  rewrite -(leq_add2r (y1S + x2S)); applyr P3.

  rewrite -(leq_add2r y2S); applyr P4.

  applyl x2y2SE; applyl x1Sy1SE.

  rewrite -[in 2 × a](prednK a_gt0).

  applyr F4n; applyr F4n1; gsimpl.

  rewrite (maxn_idPr _) //.

  rewrite -(leq_add2r (S_[1] n.+1 + S_[b.+1] n.+1)); applyl F5n.

  rewrite -(leq_add2r (S_[1] n.+2 + S_[b.+1] n.+2)); applyl F5n1.

  gsimpl.

  rewrite -(leq_add2r (S_[1] n.+1)); applyl F6n; gsimpl.

  rewrite F71; gsimpl.

  rewrite !add1n {}F73; gsimpl.

  rewrite -(leq_add2r (S_[1] n.+2 + S_[2] n.+2)).

  applyl F6n1; gsimpl.

  rewrite {}F72 {}F721 {}F711 {}F71; gsimpl.

  applyl F8.

  by applyl F9; gsimpl.

rewrite negb_and -leqNgt -ltnNgeoH.

have [/andP[a_gt1 /eqP bE1]|] := boolP ((1 < a) && (b == 1)).

  have am1_gt0 : 0 < a.-1 by rewrite -subn1 subn_gt0.

  have lEa : l = a.

    have : a + b = l.+1 by rewrite addnC subnK //.

    by rewrite bE1 addn1 ⇒ [] [].

  have uaiLEp2 : u ai ldisk = p2.

    have /cH/subsetP/(_ (u ai ldisk) (codom_f _ _)) : 0 < ai < l.+1.

      by rewrite aiE a_gt0 lEa /=.

    by rewrite !inE aiE (negPf aH) orbF ⇒ /eqP.

  pose si i : configuration 4 n.+1 :=
     sgdist1 p2 (u (inord i)) (u (inord i.+1)).

  pose ti i : configuration 4 n.+1 :=
     sgdist2 p2 (u (inord i)) (u (inord i.+1)).

  have sitiH i : i < a.-1
     [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
         codom (ti i) \subset [:: u (inord i) ldisk; p2] &
         `d[u (inord i), u (inord i.+1)]_smove =
           D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].

    moveiLa.

    have iLa1 : i < a by rewrite (leq_trans iLa) // ssrnat.leq_pred.

    apply: sgdistE ⇒ //.

    - by rewrite aMin1.

    - rewrite !aMin1 //; last by rewrite -[a]prednK.

      by rewrite apegS apeg_eqC.

    - by rewrite aMin1 1?eq_sym // -[a]prednK.

    - by rewrite aMin1.

    by rewrite aMin1 // -[a]prednK.

  pose pa := a[p1, p3] a.

  pose sam1 : configuration 4 n.+1 := sgdist1 pa (u (inord a.-1)) (u (inord a)).

  pose tam1 : configuration 4 n.+1 := sgdist2 pa (u (inord a.-1)) (u (inord a)).

  have [sam1C tam1C duam1ua1E] :
     [/\ codom sam1 \subset [:: pa; u (inord a) ldisk ],
         codom tam1 \subset [:: u (inord a.-1) ldisk; pa] &
         `d[u (inord a.-1), u (inord a)]_smove =
           D[[:: ↓[u (inord a.-1)]; sam1; tam1; ↓[u (inord a)]]].+2].

    apply: sgdistE; rewrite /pa //.

    - by rewrite aMin1 ?prednK // -{2}[a]prednK //= apegS apeg_eqC.

    - by rewrite uaiLEp2 aMin1 // prednK.

    - by rewrite uaiLEp2.

    - by rewrite aMin1 // prednK.

    by rewrite uaiLEp2.

  have {}tam1C : codom tam1 \subset [:: p1; p3].

    move: tam1C; rewrite aMin1; last by rewrite -{2}[a]prednK.

    by rewrite /pa -{2}[a]prednK // apegS codom_apeg.

  pose u1 :=
    [ffun i
    if ((i : 'I_(3 × a).-2.+1) == 3 × a.-1 :>nat) then ↓[u (inord a.-1)]
    else if (i == (3 × a.-1).+1 :>nat) then sam1
    else if (i %% 3) == 0 then ↓[u (inord (i %/ 3))]
    else if (i %% 3) == 1 then si (i %/ 3)
    else ti (i %/ 3)].

  have u10E : u1 ord0 = ↓[u ord0].

    rewrite ffunE /= ifN ?inord_eq0 //.

    by rewrite neq_ltn muln_gt0 /= -ltnS prednK //= a_gt1.

  have uiME : u1 ord_max = sam1.

    rewrite ffunE /= eqn_leq leqNgt -{2}[a]prednK // mulnS.

    rewrite addSn add2n ltnS leqnn /=.

    by rewrite -{1}[a]prednK // mulnS eqxx.

  pose u2 :=
    [ffun i : 'I_4
    if i == 0 :> nat then sam1 else
    if i == 1 :> nat then tam1 else
    if i == 2 :> nat then ↓[u ai] else ↓[u (inord (l.+1))]].

  have P1 : a.*2 + sd u1 + sd u2 sd u.

    have G b1 : b1 = a
      \sum_(i < (3 × b1).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove =
      \sum_(i < (3 × a.-1)) `d[u1 (inord i), u1 (inord i.+1)]_smove +
      `d[↓[u (inord a.-1)], sam1]_smove.

      moveb1Ea.

      have ta2E : (3 × b1).-2 = (3 × a.-1).+1.

        by rewrite b1Ea -{1}[a]prednK // mulnS.

      rewrite ta2E big_ord_recr /=; congr (_ + `d[_,_]_smove).

        by rewrite ffunE ifT// inordK // -{2}b1Ea ?ta2E.

      rewrite ffunE inordK; last by rewrite -{2}b1Ea ?ta2E.

      by rewrite eqn_leq ltnn /= eqxx.

    rewrite {}[sd u1]G //.

    have → := @sum3E _ (fun i`d[u1 (inord i), u1 (inord i.+1)]_smove).

    have → : a.*2 = 2 + \sum_(i < a.-1) 2.

      rewrite sum_nat_const /= cardT size_enum_ord.

      by rewrite muln2 -(doubleD 1) add1n prednK.

    rewrite !addnA -[2 + _ + _]addnA -big_split /=.

    rewrite [sd u2]big_ord_recr /=.

    rewrite [u2 (inord 2)]ffunE inordK //=.

    rewrite [u2 (inord 3)]ffunE inordK //=.

    rewrite [2 + _]addnC -!addnA 2![X in _ + X _]addnA addnA.

    have → : sd u =
      \sum_(i < a.-1) (`d[u (inord i), u (inord i.+1)]_smove) +
      `d[u (inord a.-1), u ai]_smove + `d[u ai, u (inord ai.+1)]_smove.

      rewrite -lEa (_ : ai = inord l); last first.

        by apply/val_eqP; rewrite /= aiE inordK // lEa.

      case: l l_gt0 u ⇒ //= l1 _ f.

      rewrite /sd 2!big_ord_recr //=; congr (_ + _ + `d[f _, f _]_smove).

      by apply/val_eqP; rewrite /= !inordK.

    apply: leq_add; first apply: leq_add.

    - rewrite leq_eqVlt; apply/orP; left; apply/eqP.

      apply: eq_bigri _.

      have → : u1 (inord (3 × i)) = ↓[u (inord i)].

        rewrite ffunE inordK; last first.

          rewrite ltnS (leq_trans (_ : _ 3 × (a.-1))) //.

            by rewrite leq_mul2l /= ltnW.

          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.

        rewrite eqn_mul2l /= eqn_leq [_ i]leqNgt ltn_ord andbF.

        rewrite eqn_leq ltn_mul2l /= ltnNge [i _]ltnW // andbF.

        by rewrite mod3E /= div3E.

      have → : u1 (inord (3 × i).+1) = si i.

        rewrite ffunE inordK; last first.

          rewrite ltnS (leq_trans (_ : _ 3 × (a.-1))) //.

            by rewrite ltn_mul2l /=.

          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.

        rewrite eqn_leq [_ _.+1]leqNgt.

        rewrite (leq_trans (_ : (3 × i).+2 (3 × i.+1))) ?andbF //;
               last 2 first.

        - by rewrite mulnS addSn add2n.

        - by rewrite leq_mul2l /=.

        rewrite eqn_leq !ltnS [_ 3 × i]leq_mul2l.

        by rewrite [_ i]leqNgt ltn_ord andbF mod3E /= div3E.

      have → : u1 (inord (3 × i).+2) = ti i.

        rewrite ffunE inordK; last first.

          rewrite ltnS (leq_trans (_ : _ 3 × (a.-1))) //.

            rewrite (leq_trans (_ : _ 3 × (i.+1))) //.

              by rewrite mulnS addSn add2n.

            by rewrite leq_mul2l /=.

          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.

        rewrite eqn_leq [_ _.+1]leqNgt.

        rewrite -[(3 × i).+3](mulnDr 3 1 i) leq_mul2l ltn_ord andbF.

        rewrite eqn_leq !ltnS [_ _.+1]leqNgt.

        rewrite (leq_trans (_ : (3 × i).+1 < 3 × (i.+1))) ?andbF //;
             last 2 first.

        - by rewrite mulnS addSn add2n.

        - by rewrite leq_mul2l /=.

        by rewrite mod3E /= div3E.

      have → : u1 (inord (3 × i).+3) = ↓[u (inord i.+1)].

        have → : (3 × i).+3 = 3 × (i.+1) by rewrite mulnS addSn add2n.

        rewrite ffunE inordK; last first.

          rewrite ltnS (leq_trans (_ : _ 3 × (a.-1))) //.

            by rewrite leq_mul2l /=.

          by rewrite -{2}[a]prednK // mulnS addSn add2n /= ltnW.

        rewrite eqn_mul2l /=; case: eqP ⇒ [->//|_].

        rewrite eqn_leq [_ 3 × i.+1]leqNgt ltnS leq_mul2l /= ltn_ord andbF.

        by rewrite mod3E /= div3E.

      case: (sitiH i) ⇒ //= _ _.

      by rewrite !addnA addn0 add2n.

    - rewrite leq_eqVlt; apply/orP; left; apply/eqP.

      rewrite !big_ord_recr big_ord0 //= add0n !addnA.

      have → : u2 (inord 0) = sam1 by rewrite ffunE /= inordK.

      have → : u2 (inord 1) = tam1 by rewrite ffunE /= inordK.

      have → : u2 (inord 2) = ↓[u ai] by rewrite ffunE /= inordK.

      by move: duam1ua1E; rewrite /= addn0 add2n !addnA !addSn.

    rewrite (_ : inord l.+1 = inord ai.+1); last first.

      by apply/val_eqP; rewrite /= !inordK // lEa.

    by apply/gdist_cunlift/shanoi_connect.

  set x1P1 := sd _ in P1; set x2P1 := sd _ in P1.

  set xP1 := sd _ in P1; rewrite -/xP1.

  have cH2 (k : 'I_(3 × a).-2.+1) :
      0 < k < (3 × a).-2 codom (u1 k) \subset [:: p2; a[p1, p3] k].

    move⇒ /andP[k_gt0 k_lt].

    have kL3a1 : k (3 × a.-1).

      by rewrite -ltnS (leq_trans k_lt) // -{1}[a]prednK // mulnS.

    have kLa1 : k %/ 3 a.-1.

      by rewrite -(mulKn a.-1 (isT : 0 < 3)) leq_div2r.

    rewrite ffunE; case: eqP ⇒ [kH|/eqP kH].

      rewrite kH apegMr //.

      have := @H (inord a.-1); rewrite inordK //.

        rewrite ffunE; apply.

        by rewrite -ltnS prednK // a_gt1.

      by rewrite prednK // (leq_trans aLld1).

    have k3La2 : k %/ 3 a.-2.

      rewrite -ltnS [a.-2.+1]prednK //.

      rewrite ltn_divLR // [_ × 3]mulnC.

      by move: kL3a1 kH; case: ltngtP.

    rewrite eqn_leq [_ k]leqNgt (leq_trans k_lt) ?andbF //; last first.

      by rewrite -{1}[a]prednK // mulnS addSn add2n.

    have k3La : k %/ 3 a.

      by rewrite (leq_trans kLa1) // -subn1 leq_subr.

    case: eqPk3mH.

      apply: codom_liftr.

      rewrite {2}(divn_eq k 3) k3mH addn0 [in a[_,_] _]mulnC apegMr //.

      have := @cH (inord (k %/3)); rewrite inordK; last first.

        by rewrite (leq_ltn_trans k3La).

      apply.

      rewrite (leq_ltn_trans k3La) ?ltnS ?lEa //.

      move: k_gt0; rewrite andbT {1}(divn_eq k 3) k3mH addn0 muln_gt0.

      by case/andP.

    case: eqPk3mH1.

      case: (sitiH (k %/ 3)); first by rewrite -[a.-1]prednK.

      set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp.

      set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k.

        rewrite (divn_eq k 3) k3mH1 addn1 apegS mulnC apegMr //.

        by rewrite /i !inordK ?apegS //= !ltnS lEa.

      have H2 : (k %/ 3).+1 < l.+2 by rewrite !ltnS lEa (leq_trans k3La).

      rewrite -(@aMin1 i); last first.

        by rewrite !inordK // -{2}[a]prednK // ltnS // -[a.-1]prednK.

      congr (u _ _).

      by apply/val_eqP; rewrite /= !inordK.

    rewrite codom_subC.

    case: (sitiH (k %/ 3)) ⇒ [|_]; first by rewrite -[a.-1]prednK.

    set pp := u _ _; (suff <- : pp = a[p1, p3] k by []); rewrite {}/pp.

    set i := inord _; have <- : a[p1, p3] i = a[p1, p3] k.

      have k3mH2 : k %% 3 = 2.

        have := ltn_mod k 3; move: k3mH k3mH1.

        by case: modn ⇒ // [] [|[]].

      rewrite (divn_eq k 3) k3mH2 addn2 !apegS mulnC apegMr //.

        by rewrite /i !inordK ?apegS //= !ltnS (leq_trans k3La).

      have H2 : (k %/ 3) < l.+2 by rewrite !ltnS (leq_trans k3La).

      rewrite -(@aMin1 i); last by rewrite !inordK // -{2}[a]prednK .

      congr (u _ _).

      by apply/val_eqP; rewrite /= !inordK.

  have {cH2}P2 := IH p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 cH2.

  have a3B2_gt1 : 1 < (3 × a).-2.

    rewrite -subn2 leq_subRL.

      by rewrite (leq_trans (_ : 4 3 × 2)) // leq_mul2l.

    by rewrite (leq_trans (_ : 2 3 × 2)) // leq_mul2l.

  rewrite u10E uiME apeg0 in P2.

  have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                          (leqnn _)).

  rewrite -/x1P1 in P2.

  pose paS := a[p1, p3] a.+1.

  have cH3 (k : 'I_4) :
    0 < k < 3 codom (u2 k) \subset [:: pa; a[p2, paS] k].

    case: k ⇒ [] [|[|[|]]] //= iH _; rewrite ffunE /=.

      by have := tam1C; rewrite /pa /paS !(apegS, apeg0) codom_apeg.

    apply: codom_liftr.

    have /cH : 0 < ai < l.+1 by rewrite aiE a_gt0 // lEa /=.

    by rewrite /pa /paS !(apegS, apeg0) aiE codom_subC.

  have {cH3}P3 :
    (S_[3] n.+1).*2 sd u2 + sp (u2 ord0) 3 (a[p2, paS] 0) +
                       sp (u2 ord_max) 3 (a[p2, paS] 3).

    apply: IH cH3 ⇒ //; try by rewrite /pa /paS // eq_sym.

    by rewrite /paS apegS apeg_eqC.

  have {}P3 := leq_trans P3 (leq_add (leqnn _) (leq_sum_beta _ _)).

  rewrite /pa /paS -lEa !(apegS, apeg0) in P3.

  rewrite !ffunE /= -/x2P1 (_ : inord l.+1 = ord_max) in P3; last first.

    by apply/val_eqP; rewrite /= inordK.

  rewrite [X in _ _ + X + _]sum_beta_S //= KH1 eqxx addn0.

  set xS := \sum_(_ < _) _ in P2; rewrite -/xS.

  rewrite [X in _ _ + _ + X]sum_beta_S //= KH2 mul1n.

  set yS := \sum_(i < _) _ in P3; rewrite -/yS.

  set x1S := sp _ _ _ in P2; set y1S := sp _ _ _ in P3.

  have x1Sy1SE : x1S + y1S (S_[1] n).*2 + α_[maxn (3 × a).-2 3] n.

    apply: sum_alpha_diffE ⇒ //.

    by move: sam1C; rewrite -uiME uaiLEp2 /pa apeg32E.

  rewrite (maxn_idPl _) // in x1Sy1SE; last first.

    by rewrite -subn2 ltn_subRL ltnW // (leq_mul2l 3 2).

  rewrite -addnn {1}dsum_alphaL_S in P2.

  rewrite -addnn {1}dsum_alphaL_S.

  have F4 k : S_[a.-1] k.+1 S_[(3 ×a).-2] k + a.-1.

    apply: leq_trans (dsum_alpha3l _ _) _.

    rewrite leq_add2r.

    apply: (increasingE (increasing_dsum_alphaL_l _)).

    by rewrite -{2}[a]prednK // mulnS addSn add2n /=.

  have F4n := F4 n.

  have {F4}F4n1 := F4 n.+1.

  have F6 k : S_[a.+1] k + S_[1] k S_[a.-1] k + S_[3] k.

    have := concaveEk1 1 a.-2 2 (concave_dsum_alphaL_l k).

    by rewrite add1n addn2 !prednK // [_ + S_[3] _]addnC.

  have F6n := F6 n.+1.

  have {F6}F6n1 := F6 n.+2.

  have F72 := dsum_alphaL_S 3 n.+1.

  have F721 := dsum_alphaL_S 3 n.

  have F711 := dsum_alphaL_S 1 n.+1.

  have F71 := dsum_alphaL_S 1 n.

  have F8 : α_[1] n.+2 = α_[3] n.+1 by rewrite alphaL_3E.

  have F9 : α_[1] (n.+2) (α_[1] n).*2.+2.

    apply: leq_trans (leqnSn _).

    by apply: alphaL_4_5.

  gsimpl.

  applyr P1.

  rewrite -(leq_add2r x1S); applyr P2.

  rewrite -(leq_add2r y1S); applyr P3.

  applyl x1Sy1SE; gsimpl.

  rewrite -(leq_add2r (S_[a.-1] n.+1)) -[in 2 × a](prednK a_gt0).

  applyl F4n.

  rewrite -(leq_add2r (S_[a.-1] n.+2)); applyl F4n1.

  rewrite lEa; applyr F6n.

  rewrite -(leq_add2r (S_[1] n.+2 + S_[3] n.+2)); applyr F6n1.

  rewrite {}F72 {}F711 {}F71; gsimpl.

  rewrite !add1n -{}F8.

  by applyl F9; gsimpl.

rewrite negb_and -leqNgto1H.

have [/eqP aE1| aD1] := boolP (a == 1).

  have b_gt0 : 0 < b by rewrite /b aE1 subn1.

  have bE : b = l by rewrite /b aE1 subn1.

  move: b_gt0; rewrite leq_eqVlt ⇒ /orP[/eqP bE1 | b_gt1]; last first.

    have u1C : u (inord 1) ldisk = p2.

      move: aH; rewrite aE1 apegS apeg0.

      have /cH : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK.

      move⇒ /subsetP/(_ (u (inord 1) ldisk) (codom_f _ _)).

      by rewrite !inE ⇒ /orP[] /eqP→ //; rewrite !inordK // apegS apeg0 eqxx.

    pose s0 : configuration 4 n.+1 := sgdist1 p3 (u ord0) (u (inord 1)).

    pose t0 : configuration 4 n.+1 := sgdist2 p3 (u ord0) (u (inord 1)).

    have [s0C t0C ds0t0E] :
        [/\ codom s0 \subset [:: p3; u (inord 1) ldisk ],
         codom t0 \subset [:: u ord0 ldisk; p3] &
         `d[u ord0, u (inord 1)]_smove =
           D[[:: ↓[u ord0]; s0; t0; ↓[u (inord 1)]]].+2].

      apply: sgdistE ⇒ //.

      - by rewrite /= KH1.

      - by rewrite KH1 u1C.

      - by rewrite u1C eq_sym.

      - by rewrite KH1.

      by rewrite u1C.

    pose u1 :=
      [ffun i : 'I_4
      if i == 0 :> nat then ↓[u ord0] else
      if i == 1 :> nat then s0 else
      if i == 2 :> nat then t0 else ↓[u (inord 1)]].

    pose u2 := [ffun i ↓[u (inord ((i : 'I_b.+1) + 1))]].

    have P1 : 2 + sd u1 + sd u2 sd u.

      have → : sd u =
          `d[u ord0, u (inord 1)]_smove +
          \sum_(i < b) `d[u (inord (a +i)), u (inord (a + i.+1))]_smove.

        rewrite /sd big_ord_recl /= bE.

        congr (`d[u _,u _]_smove + _).

          by apply/val_eqP; rewrite /= inordK.

        apply: eq_bigri _.

        congr (`d[u _,u _]_smove); apply/val_eqP; rewrite aE1 /= inordK //=.

          by rewrite /bump add1n !ltnS ltnW.

        by rewrite /bump add1n !ltnS.

      apply: leq_add.

        rewrite leq_eqVlt; apply/orP; left; apply/eqP.

        rewrite /sd !big_ord_recr /= big_ord0 add0n.

        rewrite !ffunE !inordK //= add2n.

        by rewrite ds0t0E /= addn0 !addnA.

      apply: leq_sumi _.

      rewrite ffunE inordK; last by rewrite ltnS ltnW.

      rewrite ffunE inordK; last by rewrite ltnS.

      rewrite aE1 addSn [i + _]addnC addnS.

      by apply/gdist_cunlift/shanoi_connect.

    set x1P1 := sd _ in P1; set x2P1 := sd _ in P1.

    set xP1 := sd _ in P1; rewrite -/xP1.

    have cH2 (k : 'I_4) :
      0 < k < 3 codom (u1 k) \subset [:: p3; a[p1, p2] k].

      case: k ⇒ [] [|[|[|]]] //= iH _; rewrite ffunE /= !(apegS, apeg0).

        by have := s0C; rewrite u1C.

      by rewrite codom_subC -KH1.

    have {cH2}P2 :
      (S_[3] n.+1).*2 sd u1 + sp ↓[u (inord 0)] 3 (a[p1, p2] 0) +
                         sp ↓[u (inord 1)] 3 (a[p1, p2] 3).

      apply: leq_trans (IH _ _ _ _ _ _ cH2) _ ⇒ //.

        by rewrite eq_sym.

      repeat apply: leq_add ⇒ //; rewrite leq_eqVlt;
             apply/orP; left; apply/eqP.

        by apply: eq_bigri _; rewrite !ffunE inord_eq0.

      by apply: eq_bigri _; rewrite !ffunE.

    have {}P2 := leq_trans P2
               (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)).

    rewrite -/x2P1 (inord_eq0) // -[in inord 1]aE1 !(apegS, apeg0) in P2.

    have cH3 (k : 'I_b.+1) :
      0 < k < b codom (u2 k) \subset [:: p2; a[p3, p1] k].

      rewrite [X in k < X]bE ⇒ /andP[k_gt0 kLb].

      rewrite ffunE addn1; apply: codom_liftr.

      have := @cH (inord k.+1).

      rewrite inordK ?apegS //=; first by apply.

      by rewrite ltnS (leq_trans kLb).

    have {cH3}P3 :
     (S_[b] n.+1).*2 sd u2 + sp ↓[u (inord 1)] b p3 +
                        sp ↓[u ord_max] b (a[p3, p1] b).

      apply: leq_trans (IH _ _ _ _ _ _ cH3) _ ⇒ //; try by rewrite eq_sym.

      repeat apply: leq_add ⇒ //; rewrite leq_eqVlt;
         apply/orP; left; apply/eqP; apply: eq_bigri _.

        by rewrite !ffunE.

      rewrite !ffunE /= addn1 bE; congr ((u _ _ != _) × _).

      by apply/val_eqP; rewrite /= inordK.

    have {}P3 := leq_trans P3 (leq_add (leqnn _) (leq_sum_beta _ _)).

    rewrite -/x2P1 (_ : a[p3, p1] b = a[p3, p1] l) in P3; last first.

      by rewrite bE.

    rewrite -[in inord 1]aE1 in P3.

    rewrite !sum_beta_S // KH1 eqxx mul0n addn0 KH2 mul1n.

    set xS := \sum_(i < _) _ in P2; rewrite -/xS.

    set yS := \sum_(i < _) _ in P3; rewrite -/yS.

    set x1S := sp _ _ _ in P2; set y1S := sp _ _ _ in P3.

    have x1Sy1SE : x1S + y1S (S_[1] n).*2 + α_[maxn 3 b] n.

      apply: sum_alpha_diffE ⇒ //.

      apply: codom_liftr.

      have /cH : 0 < (inord a : 'I_l.+2) < l.+1 by rewrite aE1 inordK.

      by rewrite inordK aE1.

    rewrite -/x1P1 in P2.

    rewrite -addnn {1}dsum_alphaL_S -bE.

    gsimpl; applyr P1.

    rewrite -(leq_add2r x1S); applyr P2.

    rewrite -(leq_add2r y1S); applyr P3.

    applyl x1Sy1SE; gsimpl.

    move: b_gt1; rewrite leq_eqVlt ⇒ /orP[/eqP bE2|b_gt2].

      rewrite -bE2 (maxn_idPl _) //.

      rewrite [S_[3] n.+2]dsum_alphaL_S; gsimpl.

      rewrite !alphaL_3E.

      have F := leq_dsum_alpha_2l_1 n.+1; applyr F.

      rewrite !dsum_alphaL_S; gsimpl.

      rewrite !add1n.

      by have F := alphaL_4_5 n; applyl F; gsimpl.

    rewrite (maxn_idPr _) //.

    changer (2 × (S_[3] (n.+1)).+1 + 2 × S_[b] (n.+1)).

    rewrite -dsum_alpha3_S.

    rewrite ![in X in _ 2 × X + _]dsum_alphaL_S; gsimpl.

    rewrite [in X in _ _ + X]mul2n -addnn.

    rewrite [in X in _ _ + (X + _)]dsum_alphaL_S; gsimpl.

    changer ((S_[b] n + (α_[1] n).*2) + (S_[b] n.+1 + (α_[1] n.+1).*2)).

    by apply: leq_add; apply: dsum_alphaL_alpha; apply: ltnW.

  have /cH : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK.

  move⇒ /subsetP /(_ (u (inord 1) ldisk) (codom_f _ _)).

  rewrite !inE inordK // apegS apeg0.

  have := aH; rewrite (_ : inord a = inord 1); last first.

    by apply/val_eqP; rewrite /= !inordK // aE1.

  rewrite aE1 apegS ⇒ /negPf->; rewrite orbF ⇒ /eqP u1LE.

  case: (@sgdistE _ p3 (u ord0) (u (inord 1))) ⇒ //.

  - by rewrite KH1.

  - by rewrite KH1 u1LE.

  - by rewrite u1LE eq_sym.

  - by rewrite KH1.

  by rewrite u1LE.

  set s0 := sgdist1 _ _ _; set t0 := sgdist2 _ _ _.

  moves0C t0C du0u1; rewrite /= !addnA addn0 in du0u1.

  pose u1 :=
    [ffun i
      if (i : 'I_5) == 0 :> nat then ↓[u ord0] else
      if i == 1 :> nat then s0 else
      if i == 2 :> nat then t0 else
      if i == 3 :> nat then ↓[u (inord 1)] else ↓[u (inord 2)]].

  have P1 : 2 + sd u1 sd u.

    rewrite /sd 2![in X in X _]big_ord_recr
                  [X in _ X]big_ord_recr /= !addnA.

    apply: leq_add; last first.

      apply: leq_trans (gdist_cunlift _); last by apply: shanoi_connect.

      rewrite leq_eqVlt; apply/orP; left; apply/eqP.

      rewrite !ffunE ![in LHS]inordK //=.

      by congr(`d[↓[u _],↓[u _]]_smove);
         apply/val_eqP; rewrite /= !inordK //= -bE bE1.

    rewrite leq_eqVlt; apply/orP; left; apply/eqP.

    rewrite !big_ord_recr big_ord0 /= !ffunE !inordK //= add0n.

    rewrite -addnA add2n -du0u1.

    move: bE; rewrite -bE1.

    case: (l) u ⇒ // [] [] // uu _; rewrite big_ord_recl big_ord0 addn0 /=.

    by congr(`d[uu _, uu _]_smove); apply/val_eqP; rewrite /= !inordK.

  have cH1 (k : 'I_5) :
    0 < k < 4 codom (u1 k) \subset [:: p3; a[p1, p2] k].

    case: k ⇒ [] [|[|[|[|]]]] //= iH _; rewrite !ffunE !(apegS, apeg0).

    - by have := s0C; rewrite u1LE.

    - by rewrite codom_subC -KH1.

    rewrite codom_subC.

    apply/subsetPi /codomP[x ->]; rewrite !ffunE.

    have /cH: 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK //.

    by rewrite inordK // ⇒
        /subsetP /(_ (u (inord 1) (trshift 1 x)) (codom_f _ _)).

  have {cH1}P2 :
     (S_[4] n.+1).*2 sd u1 + sp (u1 ord0) 4 p1 + sp (u1 ord_max) 4 p1.

    by apply: IH cH1 ⇒ //; rewrite eq_sym.

  set xP := sd _; rewrite -/xP in P1.

  have {}P2 :=
    leq_trans P2 (leq_add (leq_add (leqnn _ ) (leq_sum_beta _ _))
                          (leq_sum_beta _ _)).

  set x1P := sd _ in P1; rewrite -/x1P in P2.

  rewrite !ffunE /= (_ : inord 2 = ord_max) in P2; last first.

    by apply: val_inj; rewrite /= inordK // -bE bE1.

  rewrite {2}(_ : p1 = a[p3, p1] l) in P2; last first.

    by rewrite -bE -bE1.

  set x1S := \sum_(_ < _) _ in P2; set x2S := \sum_(_ < _) _ in P2.

  rewrite !sum_beta_S //= KH1 KH2 !eqxx !addn0 mul1n.

  rewrite -/x1S -/x2S -!addnA.

  apply: leq_trans (leq_add P1 (leqnn _)).

  rewrite -!addnA addnC !addnA -addnA.

  apply: leq_trans (leq_add P2 (leqnn _)).

  rewrite -bE -bE1 -addnn {2}dsum_alphaL_S addnA.

  rewrite [_ + 2]addnC !addnA leq_add2r addnC.

  by apply: leq_dsum_alpha_2l_l 2 n.+1.

have aEl : a = l.+1.

  apply/eqP; rewrite eqn_leq aLld1 /=.

  case/orP: oH; first by case: (a) aD1 a_gt0 ⇒ [|[|]].

  case/orP: o1H; first by case: (a) aD1 a_gt0 ⇒ [|[|]].

  rewrite /b prednK // ⇒ H1 lLa; move: lLa H1.

  by rewrite leq_eqVlt ⇒ /orP[] // /eqP ->; rewrite subSn // subnn eqxx.

have bE0 : b = 0 by rewrite /b aEl subnn.

pose si i : configuration 4 n.+1 :=
  sgdist1 p2 (u (inord i)) (u (inord i.+1)).

pose ti i : configuration 4 n.+1 :=
   sgdist2 p2 (u (inord i)) (u (inord i.+1)).

have sitiH i : i < l
   [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
       codom (ti i) \subset [:: u (inord i) ldisk; p2] &
       `d[u (inord i), u (inord i.+1)]_smove =
         D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].

  moveiLl.

  have iLl1 : i < l.+1 by rewrite (leq_trans iLl).

  apply: sgdistE ⇒ //.

  - by rewrite aMin1 // aEl.

  - rewrite !aMin1 ?aEl //.

    by rewrite apegS apeg_eqC.

  - by rewrite aMin1 ?aEl // eq_sym.

  - by rewrite aMin1 // aEl.

  by rewrite aMin1 // aEl.

pose u1 :=
  [ffun i
    if ((i : 'I_(3 × l).+2) == (3 × l).+1 :>nat) then ↓[u ai]
    else if (i %% 3) == 0 then ↓[u (inord (i %/ 3))]
    else if (i %% 3) == 1 then si (i %/ 3)
    else ti (i %/ 3)].

have u10E : u1 ord0 = ↓[u ord0].

  rewrite ffunE /=.

  by congr (↓[u _]); apply/val_eqP; rewrite /= inordK.

have u1mE : u1 ord_max = ↓[u ord_max].

  rewrite ffunE eqxx.

  by congr (↓[u _]); apply/val_eqP/eqP; rewrite /= inordK.

have P1 : l.*2 + sd u1 sd u.

  rewrite /sd !big_ord_recr /=.

  rewrite addnA; apply: leq_add; last first.

    apply: leq_trans (gdist_cunlift _); last by apply: shanoi_connect.

    rewrite leq_eqVlt; apply/orP; left; apply/eqP.

    rewrite !ffunE !inordK ?eqxx //.

    rewrite eqn_leq [_ _ × _]leqNgt leqnn andbF mod3E /= div3E.

    congr (`d[↓[u _], ↓[u _]]_smove); apply/val_eqP; rewrite /= ?mulKn //.

    by rewrite inordK // aiE aEl.

  rewrite leq_eqVlt; apply/orP; left; apply/eqP.

  have → := @sum3E _ (fun i`d[u1 (inord i), u1 (inord i.+1)]_smove).

  have → : l.*2 = \sum_(i < l) 2.

    by rewrite sum_nat_const /= cardT size_enum_ord muln2.

  rewrite -big_split /=; apply: eq_bigri _.

  rewrite ffunE !inordK //; last first.

    by rewrite ltnS ltnW // ltnS leq_mul2l /= ltnW.

  rewrite eqn_leq [_ _ × _]leqNgt ltnS leq_mul2l //=.

  rewrite (ltnW (ltn_ord _)) andbF mod3E /= div3E.

  rewrite ffunE !inordK //; last first.

    by rewrite !ltnS leq_mul2l /= ltnW.

  rewrite eqn_leq [_.+1 _]leqNgt !ltnS leq_mul2l /= [_ i]leqNgt.

  rewrite ltn_ord andbF mod3E /= div3E -[(_ × _).+3](mulnDr 3 1 i) add1n.

  rewrite ffunE !inordK //; last first.

    by rewrite!ltnS ltn_mul2l /=.

  rewrite !mod3E /= !div3E ifN; last first.

    case: eqP ⇒ // eH.

    have : (3 × i).+2 %% 3 = (3 × l).+1 %% 3 by rewrite eH.

    by rewrite !mod3E.

  rewrite ffunE inordK; last first.

    by rewrite ltnS ltnW // ltnS leq_mul2l /=.

  rewrite mod3E /= div3E ifN.

    case: (sitiH i) ⇒ //= _ _ →.

    by rewrite /= !addnA addn0.

  case: eqP ⇒ // eH.

  have : (3 × i.+1) %% 3 = (3 × l).+1 %% 3 by rewrite eH.

  by rewrite !mod3E.

have cH1 (k : 'I_(3 × l).+2) :
    0 < k < (3 × l).+1 codom (u1 k) \subset [:: p2; a[p1, p3] k].

  rewrite !ffunE.

  case: eqP ⇒ [->|/eqP kD3l1]; first by rewrite ltnn andbF.

  case: eqP ⇒ [km3E0|/eqP km3D0].

    rewrite {1 2 4}(divn_eq k 3) km3E0 addn0.

    rewrite ltnS mulnC muln_gt0 leq_mul2l /= ⇒ /andP[k3_gt0 k3Ll].

    rewrite apegMr //.

    have:= @H (inord (k %/ 3)); rewrite ffunE inordK //; last first.

      by apply: leq_trans k3Ll _.

    by apply; rewrite k3_gt0.

  case: eqP ⇒ [km3E1|/eqP km3D1].

    rewrite {1 2 4}(divn_eq k 3) km3E1 addn1 !ltnS /= mulnC ltn_mul2l /= ⇒ H1.

    case: (sitiH (k %/ 3)) ⇒ //.

    by rewrite apegS apegMr // aMin1 ?apegS // aEl ltnS.

  have km3E2 : k %% 3 = 2.

    by case: (_ %% _) (ltn_mod k 3) km3D0 km3D1 ⇒ // [] [|[|]].

  rewrite {1 2 4}(divn_eq k 3) km3E2 addn2 /= ltnSH1.

  have {}H1 : k %/ 3 < l.

    by rewrite -[_ < _](ltn_mul2r 3) [l × 3]mulnC (leq_ltn_trans _ H1).

  rewrite codom_subC.

  case: (sitiH (k %/ 3)) ⇒ // _.

  rewrite !apegS [_ × 3]mulnC apegMr //.

  by rewrite aMin1 // (leq_trans H1) // aEl.

have {cH1}P2 :
   (S_[(3 × l).+1] n.+1).*2 sd u1 + sp (u1 ord0) (3 × l).+1 p1 +
                               sp (u1 ord_max) (3 × l).+1
                                               (a[p1, p3] (3 × l).+1).

  by apply: IH cH1.

 have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                          (leq_sum_beta _ _)).

set xP := sd _; rewrite -/xP in P1.

set x1P := sd _ in P1.

rewrite -/x1P (_ : a[p1, p3] (3 × l).+1 = a[p3, p1] l) in P2; last first.

  by rewrite apegS apegMr.

rewrite !sum_beta_S // KH1 KH2 !eqxx addn0 mul1n.

rewrite !ffunE /= eqxx inord_eq0 // (_ : ai = ord_max) in P2; last first.

  by apply: val_inj; rewrite /= inordK.

set x1S := \sum_(_ < _) _ in P2; set x2S := \sum_(_ < _) _ in P2.

rewrite -/x1S -/x2S .

rewrite -addnn {1}dsum_alphaL_S addnAC !addnA leq_add2r.

rewrite -[X in _ X]addnA.

apply: leq_trans (leq_add P1 (leqnn _)).

rewrite -[X in _ X]addnA [x1P + _]addnA.

apply: leq_trans (leq_add (leqnn _) P2).

apply: leq_trans (leq_dsum_alpha_2l_l _ _) _.

rewrite addnC; apply: leq_add.

  by rewrite -addnn -addn1 leq_add.

rewrite leq_double.

apply: (increasingE (increasing_dsum_alphaL_l _)).

by rewrite doubleS ltnS -mul2n ltn_mul2r l_ggt0.

Qed.


End Case1.


Section Case2.


Variable n : nat.


Hypothesis IH:
      (l : nat) (p1 p2 p3 : ordinal_eqType 4)
       (u : {ffun 'I_l.+1 configuration 4 n.+1}),
     p1 != p2
     p1 != p3
     p2 != p3
     p1 != p0
     p2 != p0
     p3 != p0
     ( k : 'I_l.+1,
      0 < k < l codom (u k) \subset [:: p2; a[p1, p3] k])
     (S_[l] n.+1).*2 sd u + sp (u ord0) l (a[p1, p3] 0) +
                            sp (u ord_max) l (a[p1, p3] l).


Lemma case2 l (u : {ffun 'I_l.+2 configuration 4 n.+2})
              (p1 p2 p3: peg 4) :
   p1 != p2 p1 != p3 p2 != p3
   p1 != p0 p2 != p0 p3 != p0
  ( k : 'I_l.+2,
     0 < k < l.+1 codom (u k) \subset [:: p2; a[p1, p3] k])
  (u ord0 ord_max = p1)
  (u ord_max ord_max = a[p3, p1] l)
  ( k, u k ldisk = a[p1, p3] k)
  (S_[l.+1] n.+2).*2 sd u + sp (u ord0) l.+1 p1
                             + sp (u ord_max) l.+1 (a[p3, p1] l).

Proof.

movep1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0.

move⇒ /= cH KH1 KH2 ukLE.

pose u':= ([ffun i ↓[u i]] : {ffun 'I_l.+2 configuration 4 n.+1})
 : {ffun 'I_l.+2 configuration 4 n.+1}.

have H: k : 'I_l.+2,
    0 < k < l.+1 codom (u' k) \subset [:: p2; a[p1, p3] k].

  by movek kH; rewrite ffunE; apply/codom_liftr/cH.

have apegpaD2 a : a[p1, p3] a != p2.

  by rewrite /apeg; case: odd; rewrite // eq_sym.

have apegpaD0 a : a[p1, p3] a != p0.

  by rewrite /apeg; case: odd; rewrite // eq_sym.

pose si i : configuration 4 n.+1 :=
    sgdist1 p2 (u (inord i)) (u (inord i.+1)).

pose ti i : configuration 4 n.+1 :=
    sgdist2 p2 (u (inord i)) (u (inord i.+1)).

have sitiH i : i < l.+1
    [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
        codom (ti i) \subset [:: u (inord i) ldisk; p2] &
        `d[u (inord i), u (inord i.+1)]_smove =
          D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].

  moveiLl.

  have i1Ll1 : i l by [].

  apply: sgdistE; rewrite ?ukLE //.

    rewrite !inordK //=; last by rewrite ltnS ltnW // ltnS.

    by rewrite apegS apeg_eqC.

  by rewrite eq_sym.

pose u1 :=
  [ffun i
  if ((i : 'I_(3 × l.+1).+1) %% 3) == 0 then ↓[u (inord (i %/ 3))]
  else if (i %% 3) == 1 then si (i %/ 3)
  else ti (i %/ 3)].

have u10E : u1 ord0 = ↓[u ord0].

  rewrite ffunE /=.

  by congr (↓[u _]); apply/val_eqP; rewrite /= inordK.

have u1ME : u1 ord_max = ↓[u ord_max].

  rewrite ffunE /= mod3E /= div3E.

  by congr (↓[u _]); apply/val_eqP; rewrite /= inordK.

have P1 : l.+1.*2 + sd u1 = sd u.

  rewrite /sd.

  have → := @sum3E _ (fun i`d[u1 (inord i), u1 (inord i.+1)]_smove).

  have → : l.+1.*2 = \sum_(i < l.+1) 2.

    by rewrite sum_nat_const /= cardT size_enum_ord muln2.

  rewrite -big_split /=; apply: eq_bigri _.

  rewrite ffunE !inordK //; last first.

    by rewrite ltnS leq_mul2l ltnW.

  rewrite mod3E /= div3E.

  rewrite ffunE inordK; last first.

    by rewrite ltnS ltn_mul2l /=.

  rewrite mod3E /= div3E.

  rewrite ffunE inordK; last first.

    by rewrite -[_.+3](mulnDr 3 1) ltnW // ltnS leq_mul2l /= add1n.

  rewrite mod3E /= div3E.

  rewrite ffunE inordK; last first.

    by rewrite -[(_ × _).+3](mulnDr 3 1) ltnS leq_mul2l /=.

  rewrite -[(_ × _).+3](mulnDr 3 1) mod3E /= div3E.

  case: (sitiH i) ⇒ // _ _.

  by rewrite /= add2n addn0 !addnA add1n.

have cH1 (k : 'I_(3 × l.+1).+1) :
  0 < k < 3 × l.+1 codom (u1 k) \subset [:: p2; a[p1, p3] k].

  rewrite !ffunE.

  case: eqP ⇒ [km3E0|/eqP km3D0].

    rewrite {1 2 4}(divn_eq k 3) km3E0 addn0.

    rewrite muln_gt0 andbT [_ × 3]mulnC ltn_mul2l /= ⇒ /andP[k3_gt0 k3Ll].

    rewrite apegMr //.

    have:= @H (inord (k %/ 3)); rewrite ffunE inordK //; last first.

      by apply: leq_trans k3Ll _.

    by apply; rewrite k3_gt0.

  case: eqP ⇒ [km3E1|/eqP km3D1].

    rewrite {1 2 4}(divn_eq k 3) km3E1 addn1 /= ⇒ H1.

    have : 3 × (k %/ 3) < 3 × l.+1.

      apply: leq_trans H1; first by rewrite mulnC ltnW.

      rewrite ltn_mul2l /= ⇒ k3Ll1.

    case: (sitiH (k %/ 3)) ⇒ //.

    by rewrite apegS [_ × 3]mulnC apegMr // ukLE inordK // apegS.

  have km3E2 : k %% 3 = 2.

    by case: (_ %% _) (ltn_mod k 3) km3D0 km3D1 ⇒ // [] [|[|]].

  rewrite {1 2 4}(divn_eq k 3) km3E2 addn2 /= -[_.+3](mulnDl 1 _ 3).

  rewrite mulnC leq_mul2l /= add1nH1.

  rewrite codom_subC.

  case: (sitiH (k %/ 3)) ⇒ // _ sH _; move: sH.

  by rewrite ukLE // inordK ?(leq_trans H1) // !apegS [_ × 3]mulnC apegMr.

have {cH1}P2 :
    (S_[3 × l.+1] n.+1).*2 sd u1 + sp (u1 ord0) (3 × l.+1) p1
                                    + sp (u1 ord_max) (3 × l.+1)
                                         (a[p1, p3] (3 × l.+1)).

  by apply: IH cH1.

have {}P2 := leq_trans P2 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                        (leq_sum_beta _ _)).

rewrite [X in _ _ + X + _]big_ord_recr /= ukLE eqxx addn0.

rewrite [X in _ _ + X]big_ord_recr /= ukLE apegS eqxx addn0.

set x1S := \sum_(_ < n.+1) _ in P2; set x2S := \sum_(_ < n.+1) _ in P2.

rewrite [X in _ _ + X + _](_ : _ = x1S); last first.

  apply: eq_bigri _.

  rewrite u10E ffunE /beta ifF; last first.

    by rewrite eqn_leq [_ i]leqNgt ltn_ord !andbF.

  by congr ((u _ _ != _) × _); apply/val_eqP; rewrite /=.

rewrite [X in _ _ + X](_ : _ = x2S); last first.

  apply: eq_bigri _.

  rewrite u1ME ffunE /beta ifF; last first.

    by rewrite eqn_leq [_ i]leqNgt ltn_ord !andbF.

  congr ((u _ _ != _) × _); first by apply/val_eqP.

  by rewrite apegMr // apegS.

rewrite -P1 -!addnA addnC !addnA.

apply: leq_trans (leq_add P2 (leqnn _)).

by rewrite -doubleD leq_double dsum_alpha3l.

Qed.


End Case2.


Section Case3.


Variable n : nat.


Hypothesis IH:
   (l : nat) (p1 p2 p3 : ordinal_eqType 4)
    (u : {ffun 'I_l.+1 configuration 4 n.+1}),
  p1 != p2
  p1 != p3
  p2 != p3
  p1 != p0
  p2 != p0
  p3 != p0
  ( k : 'I_l.+1,
  0 < k < l codom (u k) \subset [:: p2; a[p1, p3] k])
  (S_[l] n.+1).*2 sd u + sp (u ord0) l p1 + sp (u ord_max) l (a[p1, p3] l).


Lemma case3 l (u : {ffun 'I_l.+2 configuration 4 n.+2})
              (p1 p2 p3: peg 4) :
   p1 != p2 p1 != p3 p2 != p3
   p1 != p0 p2 != p0 p3 != p0
  ( k : 'I_l.+2,
     0 < k < l.+1 codom (u k) \subset [:: p2; a[p1, p3] k])
  (u ord0 ord_max = p1)
  (u ord_max ord_max = a[p3, p1] l)
  (S_[l.+1] n.+2).*2 sd u + sp (u ord0) l.+1 p1
                             + sp (u ord_max) l.+1 (a[p3, p1] l).

Proof.

movep1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0.

movecH KH1 KH2.

pose u':= ([ffun i ↓[u i]] : {ffun 'I_l.+2 configuration 4 n.+1})
 : {ffun 'I_l.+2 configuration 4 n.+1}.

have H: k : 'I_l.+2,
    0 < k < l.+1 codom (u' k) \subset [:: p2; a[p1, p3] k].

  by movek kH; rewrite ffunE; apply/codom_liftr/cH.

have apegpaD2 a : a[p1, p3] a != p2.

  by rewrite /apeg; case: odd; rewrite // eq_sym.

have apegpaD0 a : a[p1, p3] a != p0.

  by rewrite /apeg; case: odd; rewrite // eq_sym.

case: (pickP (fun iu i ldisk != a[p1, p3] i)) ⇒ [x xH|pH]; last first.

  have {pH}ukLE k : u k ldisk = a[p1, p3] k by have := pH k; case: eqP.

  have := case2 _ _ _ _ _ _ _ cH KH1 KH2 ukLE.

  by apply.

have exH : x, u (inord x) ldisk != a[p1, p3] x.

   x; rewrite (_ : inord x = x) //.

  by apply/val_eqP; rewrite /= inordK.

case: (@ex_minnP _ exH) ⇒ a aH {exH}aMin.

have exL : x, (x l) && (u (inord x) ord_max != a[p1, p3] x).

   x; apply/andP; split ⇒ //.

    have := ltn_ord x.

     rewrite ltnS leq_eqVlt ⇒ /orP[] // /eqP xEl1.

    case/eqP: xH.

    rewrite (_ : x = ord_max); last by apply/val_eqP/eqP.

    by apply/eqP/val_eqP; rewrite /= apegS.

  by rewrite (_ : inord x = x) //; apply/val_eqP; rewrite /= inordK.

have exL1 y : (y l) && (u (inord y) ord_max != a[p1, p3] y) y l.

  by case/andP.

pose a1 := ex_maxn exL exL1.

have a1H: u (inord a1) ldisk != a[p1, p3] a1.

  by rewrite /a1; case: ex_maxnPi /andP[].

have a1Ll : a1 l by rewrite /a1; case: ex_maxnPi /andP[].

have a1Max i : a1 < i < l.+2 u (inord i) ord_max = a[p1, p3] i.

  case/andPa1Li; rewrite ltnS leq_eqVlt ⇒ /orP[/eqP iEl1|iLl].

    rewrite iEl1 apegS (_ : inord l.+1 = ldisk) //.

    by apply/val_eqP; rewrite /= inordK.

  move: a1Li; rewrite /a1; case: ex_maxnPj _ /(_ i).

  by case: eqP; rewrite // andbT_ /(_ iLl); rewrite ltnNge ⇒ →.

have aLld1 : a l.+1.

  rewrite -ltnS; apply: leq_trans (ltn_ord x).

  rewrite ltnS; apply: aMin;rewrite (_ : inord x = x) //.

  by apply/val_eqP; rewrite /= inordK.

wlog aLl1Ba1 : u p1 p3 p1Dp3 p2Dp3 p3Dp0 apegpaD2 apegpaD0 p1Dp2 p1Dp0
   {u' H xH exL exL1}cH KH1 KH2 a a1 aH aLld1 aMin a1H a1Ll a1Max /
  a l.+1 - a1.

  movewH.

  case: (leqP a (l.+1 -a1)) ⇒ [aLl1Ba1|l1Ba1La].

    by apply: wH aLl1Ba1.

  have a_gt0 : 0 < a by apply: leq_ltn_trans l1Ba1La.

  pose u1 : {ffun 'I_l.+2 configuration 4 n.+2} :=
     [ffun i : 'I_l.+2 u (inord (l.+1 - i))].

  have → : sd u = sd u1.

    have F : injective (fun i : 'I_l.+1 ⇒ (inord (l - i) : 'I_l.+1)).

      movei j /val_eqP.

        have lBiLl (i1 : 'I_l.+1) : l - i1 < l.+1.

          by rewrite ltn_subLR ?leq_addl // -ltnS.

      rewrite /= !inordK // ⇒ /eqP liE; apply/val_eqP ⇒ /=.

      rewrite -(subKn (_ : i l)); last by rewrite -ltnS.

      by rewrite liE subKn // -ltnS.

    rewrite [sd u](reindex_inj F) /=.

    apply: eq_bigri _; rewrite !ffunE.

    have iLl2 : i < l.+2 by apply: leq_trans (ltn_ord _) _.

    have lBiLl : l - i < l.+1 by rewrite ltn_subLR ?leq_addl // -ltnS.

    have iLl : i l by rewrite -ltnS.

    rewrite gdistC; last by apply/move_sym/ssym.

    congr (`d[u _,u _]_smove).

      by apply/val_eqP; rewrite /= !inordK ?subSn.

    by apply/val_eqP; rewrite /= !inordK // ?subSS ltnS // ltnW.

  pose p1' := a[p1, p3] l; pose p3' := a[p3, p1] l.

  have → : sp (u ord0) l.+1 p1 = sp (u1 ord_max) l.+1 (a[p1', p3'] l).

    apply: eq_bigri _; congr (_ × _).

    rewrite -apegD addnn apegO odd_double /= apegS apeg0.

    by rewrite ffunE subnn inord_eq0.

  have → : sp (u ord_max) l.+1 (a[p3, p1] l) = sp (u1 ord0) l.+1 p3'.

    apply: eq_bigri _; congr (_ × _).

    rewrite ffunE subn0.

    suff → : inord l.+1 = ord_max :> 'I_l.+2 by [].

    by apply/val_eqP; rewrite /= inordK.

  rewrite addnAC.

  have FF : (l.+1 - a1) l.+1 - (l.+1 - a).

    by rewrite leq_sub2l // leq_subLR addnC -leq_subLR ltnW.

  have a1Ll1 : a1 l.+1 by rewrite (leq_trans a1Ll).

  apply: wH FF ⇒ //.

  - by rewrite apeg_eqC eq_sym.

  - by rewrite eq_sym apeg_neq // eq_sym.

  - by rewrite apeg_neq // eq_sym.

  - by moveb; rewrite !apeg_neq // eq_sym.

  - by moveb; rewrite !apeg_neq // eq_sym.

  - by rewrite apeg_neq // eq_sym.

  - by rewrite apeg_neq // eq_sym.

  - movek /andP[kH1 kH2]; rewrite ffunE.

    have F1 : k l.+1 by apply: ltnW.

    have F2 : l.+1 - k < l.+2.

      by rewrite ltn_subLR // addnS ltnS leq_addl.

    have → : a[p3', p1'] k = a[p1, p3] (inord (l.+1 - k) : 'I_l.+2) .

      rewrite inordK // -apegD -apegS -addnS.

      by rewrite [LHS]apegO [RHS]apegO oddD oddB //= addbC.

    apply: cH; rewrite inordK // subn_gt0 // ltn_subLR // kH2 //=.

    by rewrite addnS ltnS -{1}[l.+1]add1n leq_add2r.

  - rewrite !ffunE /p1' subn0 -[RHS]KH2; congr (u _ _); apply/val_eqP.

    by rewrite /= inordK.

  - by rewrite !ffunE /p1' subnn inord_eq0 // KH1 /p3' -apegD addnn apeg_double.

  - rewrite ffunE inordK //=; last by rewrite ltnS leq_subr.

    rewrite subKn // -apegD apegO oddD oddB //= addbAC !addNb addbb /=.

    by rewrite -oddS -apegO apegS.

  - by rewrite leq_subr.

  - movek; rewrite ffunE.

    case: leqP ⇒ //; rewrite ltn_subRL addnC -ltn_subRLkH.

    have kLl1 : k < l.+1 by rewrite -subn_gt0 (leq_ltn_trans _ kH).

      rewrite inordK; last by rewrite ltnS ltnW.

      have /a1Max→ : a1 < l.+1 - k < l.+2 by rewrite kH /= ltnS leq_subr.

    case/eqP; rewrite -apegD apegO oddB 1?ltnW // -oddD -apegO.

    by rewrite addSn addnC apegS.

  - rewrite ffunE inordK ?ltnS ?leq_subr //.

    rewrite subKn //.

    rewrite -apegD apegO oddD oddB //= !addNb addbAC addbb /=.

    by rewrite -oddS -apegO apegS.

  - by rewrite -[a]prednK // subSS leq_subr.

  movek /andP[l1BaLk kLl2]; rewrite ffunE.

  rewrite inordK //; apply/eqP; case: eqP ⇒ // /eqP.

  suff → : a[p3', p1'] k = a[p1, p3] (l.+1 - k).

    by move⇒ /aMin; rewrite leqNgt ltn_subLR // addnC -ltn_subLR // l1BaLk.

  by rewrite [RHS]apegO oddB // -oddD -apegO addSn apegS addnC apegD.

pose u':= ([ffun i ↓[u i]] : {ffun 'I_l.+2 configuration 4 n.+1})
 : {ffun 'I_l.+2 configuration 4 n.+1}.

have H: k : 'I_l.+2,
    0 < k < l.+1 codom (u' k) \subset [:: p2; a[p1, p3] k].

  by movek kH; rewrite ffunE; apply/codom_liftr/cH.

have aMin1 i : i < a u (inord i) ord_max = a[p1, p3] i.

  by case: (u (inord i) ord_max =P a[p1, p3] i) ⇒ // /eqP /aMin; case: leqP.

have a_gt0 : 0 < a.

  have : 0 a by [].

  rewrite leq_eqVlt ⇒ /orP[/eqP aE0|] //.

  by case/eqP: aH; rewrite inord_eq0 // -aE0.

pose ai : 'I_l.+2 := inord a.

have aiE : ai = a :> nat by rewrite inordK.

have aLa1 : a a1.

  case: leqP ⇒ // ⇒ a1La.

  by case/eqP: aH; apply: a1Max; rewrite a1La.

have uaLEp2 : u (inord a) ldisk = p2.

  have /cH : 0 < (inord a : 'I_l.+2) < l.+1.

    by rewrite inordK // a_gt0 /= (leq_ltn_trans _ (_ : a1 < l.+1)).

  move⇒ /subsetP/(_ (u (inord a) ldisk) (codom_f _ _)).

  by rewrite !inE inordK // (negPf aH) orbF ⇒ /eqP.

have ua1LEp2 : u (inord a1) ldisk = p2.

  have /cH : 0 < (inord a1 : 'I_l.+2) < l.+1.

    by rewrite inordK // !ltnS (leq_trans a1Ll) // (leq_trans a_gt0).

  move⇒ /subsetP/(_ (u (inord a1) ldisk) (codom_f _ _)).

  by rewrite !inE inordK ?ltnS ?(leq_trans a1Ll) // (negPf a1H) orbF ⇒ /eqP.

have a1_gt0 : 0 < a1 by apply: leq_trans a_gt0 _.

pose b := a1 - a.

pose c := l.+1 - a1.

have c_gt0 : 0 < c by rewrite subn_gt0.

have l1E : l.+1 = a + b + c.

  by rewrite /b /c [a + _]addnC subnK // addnC subnK // ltnW.

pose si i : configuration 4 n.+1 :=
   sgdist1 p2 (u (inord i)) (u (inord i.+1)).

pose ti i : configuration 4 n.+1 :=
   sgdist2 p2 (u (inord i)) (u (inord i.+1)).

have sitiH i : i < a.-1
   [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
       codom (ti i) \subset [:: u (inord i) ldisk; p2] &
       `d[u (inord i), u (inord i.+1)]_smove =
         D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].

  moveiLa.

  have iLa1 : i < a by rewrite (leq_trans iLa) // ssrnat.leq_pred.

  apply: sgdistE; rewrite ?aMin1 // -1?[a]prednK //.

    by rewrite apegS apeg_eqC.

  by rewrite eq_sym.

pose pa := a[p1, p3] a.

pose sam1 : configuration 4 n.+1 := sgdist1 pa (u (inord a.-1)) (u (inord a)).

pose tam1 : configuration 4 n.+1 := sgdist2 pa (u (inord a.-1)) (u (inord a)).

have [sam1C tam1C duam1ua1E] :
   [/\ codom sam1 \subset [:: pa; u (inord a) ldisk ],
       codom tam1 \subset [:: u (inord a.-1) ldisk; pa] &
       `d[u (inord a.-1), u (inord a)]_smove =
         D[[:: ↓[u (inord a.-1)]; sam1; tam1; ↓[u (inord a)]]].+2].

  apply: sgdistE; rewrite /pa ?uaLEp2 ?aMin1 ?prednK //.

  by rewrite -{2}(prednK a_gt0) apegS apeg_eqC.

rewrite uaLEp2 in sam1C.

have {}tam1C : codom tam1 \subset [:: p1; p3].

  move: tam1C; rewrite aMin1; last by rewrite -{2}[a]prednK.

  by rewrite /pa -{2}[a]prednK // apegS codom_apeg.

pose u1 :=
  [ffun i : 'I_(3 × a).+1
  if (i %% 3) == 0 then ↓[u (inord (i %/ 3))]
  else if (i %% 3) == 1 then
     (if i == (3 × a.-1).+1 :> nat then sam1 else si (i %/ 3))
  else
     (if i == (3 × a.-1).+2 :> nat then tam1 else ti (i %/ 3))].

have u10E : u1 ord0 = ↓[u ord0] by rewrite ffunE /= inord_eq0.

have uiME : u1 ord_max = ↓[u (inord a)] by rewrite ffunE /= mod3E /= div3E.

have P1 : a.*2 + sd u1 = \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove.

  rewrite /sd.

  have → := @sum3E _ (fun i`d[u1 (inord i), u1 (inord i.+1)]_smove).

  have → : a.*2 = \sum_(i < a) 2.

    by rewrite sum_nat_const /= cardT size_enum_ord muln2.

  rewrite -big_split /=.

  apply: eq_bigri _.

  have → : u1 (inord (3 × i)) = ↓[u (inord i)].

    rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /= ltnW.

    by rewrite mod3E /= div3E.

  have → : u1 (inord (3 × i).+3) = ↓[u (inord i.+1)].

    rewrite -[(_ × _).+3](mulnDr 3 1).

    rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /=.

    by rewrite mod3E /= div3E.

  have [/eqP iEa| iDa] := boolP (i == a.-1 :> nat).

    have → : u1 (inord (3 × i).+1) = sam1.

      rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=.

      rewrite mod3E /= div3E.

      by rewrite iEa eqxx.

    have → : u1 (inord (3 × i).+2) = tam1.

      rewrite ffunE inordK; last first.

        by rewrite -[_.+3](mulnDr 3 1) ltnW // add1n ltnS leq_mul2l /=.

      rewrite mod3E /= div3E.

      by rewrite iEa eqxx.

    by rewrite iEa prednK // duam1ua1E /= -!addnA add2n !addnA addn0.

  have → : u1 (inord (3 × i).+1) = si i.

    rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=.

    rewrite mod3E /= div3E.

    by rewrite [_.+1 == _.+1]eqn_mul2l /= (negPf iDa).

  have → : u1 (inord (3 × i).+2) = ti i.

    rewrite ffunE inordK; last first.

      by rewrite -[_.+3](mulnDr 3 1) ltnW // ltnS add1n leq_mul2l /=.

    rewrite mod3E /= div3E.

    by rewrite [_.+1 == _.+1]eqn_mul2l /= (negPf iDa).

  case: (sitiH i) ⇒ // [|_ _ ->].

    rewrite -ltnS prednK //.

    have := ltn_ord i; rewrite leq_eqVlt ⇒ /orP[] //.

    by rewrite -{2}[a]prednK // [_ == _](negPf iDa).

  by rewrite /= -!addnA add2n addn0.

have sitiHb i : a1 < i < l.+1
   [/\ codom (si i) \subset [:: p2; u (inord i.+1) ldisk ],
       codom (ti i) \subset [:: u (inord i) ldisk; p2] &
       `d[u (inord i), u (inord i.+1)]_smove =
         D[[:: ↓[u (inord i)]; si i; ti i; ↓[u (inord i.+1)]]].+2].

  move⇒ /andP[a1Li iLl].

  apply: sgdistE ⇒ //;
      rewrite !a1Max ?a1Li ?(leq_trans a1Li) // ?(leq_trans iLl) //.

    by rewrite apegS apeg_eqC.

  by rewrite eq_sym.

pose sa1 : configuration 4 n.+1 :=
  sgdist1 (a[p1, p3] a1) (u (inord a1)) (u (inord a1.+1)).

pose ta1 : configuration 4 n.+1 :=
  sgdist2 (a[p1, p3] a1) (u (inord a1)) (u (inord a1.+1)).

have [sa1C ta1C dua1uad1E] :
   [/\ codom sa1 \subset [:: a[p1, p3] a1; u (inord a1.+1) ldisk ],
       codom ta1 \subset [:: u (inord a1) ldisk; a[p1, p3] a1] &
       `d[u (inord a1), u (inord a1.+1)]_smove =
         D[[:: ↓[u (inord a1)]; sa1 ; ta1; ↓[u (inord a1.+1)]]].+2].

  apply: sgdistE; rewrite ?ua1LEp2 ?a1Max ?leqnn // 1?eq_sym //.

  by rewrite apegS apeg_eqC eq_sym.

rewrite ua1LEp2 in ta1C.

have {}sa1C : codom sa1 \subset [:: p1; p3].

  move: sa1C; rewrite a1Max //; last by rewrite leqnn.

  by rewrite apegS codom_apeg.

pose u2 :=
  [ffun i : 'I_(3 × c).+1
  if (i %% 3) == 0 then ↓[u (inord (a1 +(i %/ 3)))]
  else if (i %% 3) == 1 then
     (if i == 1 :> nat then sa1 else si (a1 + (i %/ 3)))
  else
     (if i == 2 :> nat then ta1 else ti (a1 + (i %/ 3)))].

have u20E : u2 ord0 = ↓[u (inord a1)] by rewrite ffunE /= addn0.

have u2ME : u2 ord_max = ↓[u ord_max].

  rewrite ffunE /= mod3E /= div3E addnC subnK //.

    by rewrite (_ : inord _ = ord_max) //; apply/val_eqP; rewrite /= inordK.

  by rewrite ltnW // ltnS.

have P2 : c.*2 + sd u2 =
  \sum_(a1 i < l.+1) `d[u (inord i), u (inord i.+1)]_smove.

  have → : \sum_(a1 i < l.+1) `d[u (inord i), u (inord i.+1)]_smove =
            \sum_(i < c) `d[u (inord (a1 + i)), u (inord (a1 + i).+1)]_smove.

    rewrite -{1}[a1]add0n big_addn big_mkord.

    by apply: eq_bigri _; rewrite addnC.

  rewrite /sd.

  have → := @sum3E _ (fun i`d[u2 (inord i), u2 (inord i.+1)]_smove).

  have → : c.*2 = \sum_(i < c) 2.

    by rewrite sum_nat_const /= cardT size_enum_ord muln2.

  rewrite -big_split /=.

  apply: eq_bigri _.

  have → : u2 (inord (3 × i)) = ↓[u (inord (a1 + i))].

    rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /= ltnW.

    by rewrite mod3E /= div3E.

  have → : u2 (inord (3 × i).+3) = ↓[u (inord (a1 + i).+1)].

    rewrite -[(_ × _).+3](mulnDr 3 1).

    rewrite ffunE inordK; last by rewrite ltnS leq_mul2l /=.

    by rewrite mod3E /= div3E // add1n addnS.

  have [/eqP iEa| iDa] := boolP (i == 0 :> nat).

    have → : u2 (inord (3 × i).+1) = sa1.

      rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=.

      rewrite mod3E /=.

      by rewrite iEa eqxx.

    have → : u2 (inord (3 × i).+2) = ta1.

      rewrite ffunE inordK; last first.

        by rewrite -[_.+3](mulnDr 3 1) ltnW // add1n ltnS leq_mul2l /=.

      rewrite mod3E /=.

      by rewrite iEa eqxx.

    by rewrite iEa !addn0 // dua1uad1E /= -!addnA add2n !addnA addn0.

  have → : u2 (inord (3 × i).+1) = si (a1 + i).

    rewrite ffunE inordK; last by rewrite ltnS ltn_mul2l /=.

    rewrite mod3E /= div3E.

    by rewrite [_.+1 == _.+1](eqn_mul2l 3 _ 0) /= (negPf iDa).

  have → : u2 (inord (3 × i).+2) = ti (a1 + i).

    rewrite ffunE inordK; last first.

      by rewrite -[_.+3](mulnDr 3 1) ltnW // ltnS add1n leq_mul2l /=.

    rewrite mod3E /= div3E.

    by rewrite [_.+1 == _.+1](eqn_mul2l 3 _ 0) /= (negPf iDa).

  case: (sitiHb (a1 + i)) ⇒ // [|_ _ ->].

    rewrite -addn1 leq_add2l lt0n iDa /= -[l.+1](subnK (_ : a1 l.+1)).

      by rewrite addnC ltn_add2r.

    by rewrite ltnW.

  by rewrite /= -!addnA add2n addn0.

have P3 :
     \sum_(a i < a1) `d[↓[u (inord i)], ↓[u (inord i.+1)]]_smove
     \sum_(a i < a1) `d[u (inord i), u (inord i.+1)]_smove.

  apply: leq_sumi _.

  by apply: gdist_cunlift; apply: shanoi_connect.

have SH : 2 l
  (S_[l.+1] n.+2).*2 S_[l.+1] n.+2 + S_[l] n.+1 + (α_[1] n.+1).*2.

  movel_gt2.

  rewrite -addnn -!addnA leq_add2l.

  by apply: dsum_alphaL_alpha.

have [/andP[a_gt1 c_gt1]|] := boolP ((1 < a) && (1 < c)).

  have l_gt0 : 0 < l by rewrite -ltnS l1E (leq_trans c_gt1) // leq_addl.

  rewrite !sum_beta_S //= KH1 KH2 !eqxx !addn0.

  pose u1l := [ffun i : 'I_(3 × a).-2.+1 u1 (inord i)].

  have a3_gt1 : 1 < (3 × a).-2 by rewrite -(subnK a_gt1) addn2 !mulnS.

  have c3_gt1 : 1 < (3 × c).-2 by rewrite -(subnK c_gt1) addn2 !mulnS.

  have cH1 (k : 'I_(3 × a).-2.+1) :
    0 < k < (3 × a).-2 codom (u1l k) \subset [:: p2; a[p1, p3] k].

    move⇒ /andP[k_gt0 k3L3a].

    have k3La1 : k %/ 3 a.-1.

      have kL3a : k 3 × (a.-1).

        rewrite -[a.-1]subn1 mulnBr -ltnS -[3 ×1]/(2.+1) subnSK.

          by rewrite subn2.

        by rewrite (leq_mul2l 3 1).

      by rewrite -[a.-1](mulKn _ (_ : 0 < 3)) // leq_div2r.

    have k3Ll : k %/ 3 < l.

      rewrite -ltnS l1E (leq_trans (_ : _ < a.-1.+3)) //; last first.

        rewrite prednK // addnAC -addn2 (leq_trans (_ : _ a + c)) //.

          by rewrite leq_add2l.

        by rewrite leq_addr.

      by rewrite !ltnS ltnW // ltnS.

    rewrite !ffunE inordK //; last first.

      rewrite (leq_trans (ltn_ord _)) // -subn2 ltn_subLR.

        by rewrite add2n ltnS // ltnW.

      by rewrite (leq_trans (_ : _ < 3 × 1)) // leq_mul2l.

    rewrite {8}(divn_eq k 3) apegD [_ × 3]mulnC apegMr //=.

    case: eqP ⇒ [km3E0 /= |/eqP km3D0].

      have k3_gt0 : 0 < k %/ 3.

        case: (k: nat) k_gt0 km3E0 ⇒ // [] [|[|k1 _ _]] //.

        by rewrite (divnMDl 1 k1 (_ : 0 < 3)).

      rewrite km3E0 !apeg0.

      have /H : 0 < (inord (k %/ 3) : 'I_l.+2) < l.+1.

        rewrite inordK //.

          by rewrite k3_gt0 /= (leq_trans k3Ll).

        by rewrite (leq_trans k3Ll) // ltnW.

      by rewrite ffunE inordK // (leq_trans k3Ll) // ltnW .

    case: eqP ⇒ [km3E1|/eqP km3D1].

      rewrite km3E1 !apegS !apeg0; case: eqP ⇒ [->|kE3a1].

        rewrite (_ : (3 × a.-1).+1 = a.-1 × 3 + 1); last by rewrite addn1 mulnC.

        rewrite divnMDl // divn_small // addn0.

        by have := sam1C; rewrite codom_subC /pa -{1}[a]prednK //= apegS.

      move: k3La1; rewrite leq_eqVlt ⇒ /orP[/eqP k3Ea1| k3La].

        case: kE3a1.

        by rewrite (divn_eq k 3) km3E1 k3Ea1 mulnC addn1.

      case: (sitiH (k %/ 3)) ⇒ // siH _ _; move: siH.

      by rewrite aMin1 ?apegS // -{2}[a]prednK .

    have km3E2 : k %% 3 = 2.

      by case: (_ %% _) (ltn_mod k 3) km3D0 km3D1 ⇒ // [] [|[|]].

    rewrite km3E2 !apegS !apeg0; case: eqP ⇒ [kE3a1|kD3a1].

      rewrite ltnNge in k3L3a; case/negP: k3L3a.

      by rewrite kE3a1 -{1}[a]prednK // mulnS.

    move: k3La1; rewrite leq_eqVlt ⇒ /orP[/eqP k3Ea1| k3La].

      case: kD3a1.

      by rewrite (divn_eq k 3) km3E2 k3Ea1 mulnC addn2.

    rewrite codom_subC.

    case: (sitiH (k %/ 3)) ⇒ // _ tiH _; move: tiH.

    by rewrite aMin1 // -{2}[a]prednK // ltnS ltnW.

    have {cH1}P4 :
      (S_[(3 × a).-2] n.+1).*2
      \sum_(i < (3 × a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove +
      \sum_(k < n.+1) (↓[u ord0] k != p1) × β_[n.+1, (3 × a).-2] k +
      \sum_(k < n.+1) (sam1 k != pa) × β_[n.+1, (3 × a).-2] k.

    apply: leq_trans (IH _ _ _ _ _ _ cH1) _ ⇒ //.

    rewrite leq_eqVlt; apply/orP; left; apply/eqP.

    congr (_ + _ + _); apply: eq_bigri _.

    - by rewrite ![u1l _]ffunE !inordK // ltnS // ltnW.

    - by rewrite ffunE inord_eq0 // ffunE /= inord_eq0.

    rewrite !ffunE /= inordK //; last first.

      by rewrite ltnS -subn2 leq_subr.

    rewrite (_ : _.-2 = (3 × a.-1).+1); last first.

      by rewrite -{1}[a]prednK // mulnS.

    rewrite mod3E /= eqxx.

    by rewrite /pa apegS apegMr //= -apegS prednK.

  have {}P4 := leq_trans P4 (leq_add (leq_add (leqnn _)
                     (leq_sum_beta _ _)) (leqnn _)).

  set x1S := \sum_(_ < _.+1) _ in P4; set x2S := \sum_(_ < _.+1) _ in P4.

  rewrite -/x1S.

  pose u2r := [ffun i : 'I_(3 × c).-2.+1 u2 (inord i.+2)].

  pose pa1 := a[p1, p3] a1.

  pose pa1S := a[p1, p3] a1.+1.

  have cH1 (k : 'I_(3 × c).-2.+1) :
    0 < k < (3 × c).-2 codom (u2r k) \subset [:: p2; a[pa1, pa1S] k].

    move⇒ /andP[k_gt0 k3L3a].

    have k2L3c : k.+2 < (3 × c).

      by have := k3L3a; rewrite -{2}subn2 ltn_subRL add2n.

    rewrite !ffunE inordK ?ltnS 1?ltnW //.

    case: eqP ⇒ [km3E0 /= |/eqP km3D0].

      have k3_gt0 : 0 < k.+2 %/ 3.

        case: (k: nat) k_gt0 km3E0 ⇒ // [] //= k1 _ _.

        by rewrite (divnMDl 1 k1 (_ : 0 < 3)).

      have a1k3Ll1 : a1 + k.+2 %/ 3 < l.+1.

        move: k2L3c.

        rewrite {1}(divn_eq k.+2 3) km3E0 addn0 mulnC ltn_mul2l /= ⇒ k2L3c.

        rewrite -(subnK (_ : a1 l.+1)) ?(leq_trans a1Ll) //.

        by rewrite addnC ltn_add2r -/c.

      rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2 %/ 3)) ; last first.

        rewrite /pa1 /pa1S apegS -apegD -2!apegS -!addSn addnC.

        rewrite {1}(divn_eq k.+2 3) km3E0 addn0 apegO.

        by rewrite oddD odd_mul andbT -oddD -apegO.

      have /H : 0 < (inord (a1 + k.+2 %/ 3) : 'I_l.+2) < l.+1.

        rewrite inordK; first by rewrite addn_gt0 a1_gt0.

        by rewrite ltnS ltnW.

      by rewrite ffunE inordK // ltnS ltnW.

    case: eqP ⇒ [km3E1|/eqP km3D1].

      rewrite eqn_leq ltnNge /=.

      have a1La1k : a1 < a1 + k.+2 %/3.

        by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0.

      have a1k3Ll : a1 + k.+2 %/ 3 < l.+1.

        move: (ltnW k2L3c).

        rewrite {1}(divn_eq k.+2 3) km3E1 addn1 mulnC ltn_mul2l /=.

        rewrite -(subnK (_ : a1 l.+1)) ?(leq_trans a1Ll) //.

        by rewrite addnC ltn_add2r -/c.

      rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first.

        by rewrite /pa1S apegS -apegD !addnS addnC !apegS.

      rewrite (_ : a[_, _ ] _ = a[p3, p1] (a1 + (k.+2) %/ 3)) ; last first.

        rewrite apegO oddD {1}(divn_eq k.+2 3) oddD km3E1 addbT odd_mul andbT.

        by rewrite addbN -oddD -oddS -apegO apegS.

      case: (sitiHb (a1 + k.+2 %/ 3)) ⇒ // [| siH _ _].

        by rewrite a1La1k.

      by move: siH; rewrite a1Max ?apegS // ltnS ltnW.

    have km3E2 : k.+2 %% 3 = 2.

      by case: (_ %% _) (ltn_mod k.+2 3) km3D0 km3D1 ⇒ // [] [|[|]].

    rewrite ifN; last by case: (k : nat) k_gt0.

    have a1La1k : a1 < a1 + k.+2 %/3.

      by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0.

    have a1k3Ll : a1 + k.+2 %/ 3 < l.+1.

      have: k.+2 %/ 3 × 3 < 3 × c.

        rewrite ltnW //.

        move: (ltnW k2L3c).

        by rewrite {1}(divn_eq k.+2 3) km3E2 addn2.

      rewrite mulnC ltn_mul2l /=.

      rewrite -(subnK (_ : a1 l.+1)) ?(leq_trans a1Ll) //.

      by rewrite addnC ltn_add2r -/c.

    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first.

      by rewrite /pa1 /pa1S apegS -apegD addnC !addnS !apegS.

    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3)) ; last first.

      rewrite apegO /= oddD {1}(divn_eq k.+2 3) !oddD odd_mul andbT.

      by rewrite km3E2 addbF -oddD -apegO.

    rewrite codom_subC.

    case: (sitiHb (a1 + k.+2 %/ 3)) ⇒ // [| _ tiH _]; first by rewrite a1La1k.

    by move: tiH; rewrite a1Max // a1La1k ltnS ltnW.

  have P5 :
    (S_[(3 × c).-2] n.+1).*2
    \sum_(i < (3 × c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove +
    sp ta1 (3 × c).-2 pa1 + sp ↓[u ord_max] (3 × c).-2 (a[p3, p1] l).

    apply: leq_trans (IH _ _ _ _ _ _ cH1) _; rewrite /pa1 /pa1S {cH1}//.

    - by rewrite apegS apeg_eqC.

    - by rewrite eq_sym.

    repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.

    - apply: eq_bigri _.

      by rewrite ![u2r _]ffunE !inordK // ltnS // ltnW.

    - apply: eq_bigri _; congr ((_ != _) × _).

      rewrite !ffunE /= !inordK //=.

      by rewrite (leq_trans (_ : 2 < (3 × 1).+1)) // ltnS leq_mul2l.

    apply: eq_bigri _; congr ((_ != _) × _).

      rewrite !ffunE /= !prednK ?muln_gt0 //=; last first.

        by rewrite -subn1 ltn_subRL addn0 (leq_trans (_ : _ < 3 × 1)) //
                   leq_mul2l.

      rewrite inordK // mod3E /= div3E addnC subnK; last first.

        by apply: (leq_trans a1Ll).

      by rewrite ffunE; congr (u _ _ ); apply/val_eqP; rewrite /= inordK.

    rewrite -[RHS]apegS -(subnK (_ : a1 l.+1)) // -/c.

      rewrite apegS -apegD apegO oddD -subn2 oddB.

        by rewrite addbF odd_mul /= -oddD -apegO.

      by rewrite (leq_trans (_ : _ < 3 × 1)) // leq_mul2l //.

    by rewrite ltnW.

  rewrite {cH1}//.

  have {}P5 :=
    leq_trans P5 (leq_add (leqnn _) (leq_sum_beta _ _)).

  set y1S := \sum_(_ < _) _ in P5; set y2S := sp _ _ _ in P5.

  have [b_gt1|b_le2] := leqP 2 b.

    pose u3 := [ffun i : 'I_3
                 if i == 0 :> nat then sam1
                 else if i == 1 :> nat then tam1 else ↓[u (inord a)]].

    have cH6 (k : 'I_3) :
      0 < k < 2 codom (u3 k) \subset [:: p1; a[p2, p3] k].

      move⇒ /andP[k_gt0 k_lt2].

      rewrite !ffunE.

      by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 ⇒ // [] [|].

    have P6 :
      (S_[2] n.+1).*2
      (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove) + sp sam1 2 p2
                                                + sp ↓[u (inord a)] 2 p2.

      apply: (leq_trans (IH _ _ _ _ _ _ cH6)) ⇒ //.

        by rewrite eq_sym.

      repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.

      - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=.

      - by apply: eq_bigri _; rewrite !ffunE.

      by apply: eq_bigri _; rewrite !ffunE.

    rewrite {cH6}// in P6.

    set x3S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6.

    have x2Sx3SE : x2S + x3S (S_[1] n).*2 + α_[maxn (3 × a).-2 2] n.

      by apply: sum_alpha_diffE; by rewrite /pa.

    rewrite (maxn_idPl _) // in x2Sx3SE.

    pose u4 := [ffun i : 'I_b.+1 ↓[u (inord (a + i))]].

    pose paS := a[p1, p3] a.+1.

    have cH7 (k : 'I_b.+1) :
      0 < k < b codom (u4 k) \subset [:: p2; a[pa, paS] k].

      move⇒ /andP[k_gt0 k_ltb].

      have akLl : a + k < l.+1.

        rewrite ltnS (leq_trans _ a1Ll) //.

        by rewrite -(subnK aLa1) addnC leq_add2r ltnW.

      rewrite !ffunE.

      have /H : 0 < (inord (a + k) : 'I_l.+2) < l.+1.

        rewrite inordK; first by rewrite addn_gt0 a_gt0.

        by rewrite ltnS ltnW.

      rewrite ffunE inordK //; last by rewrite ltnS ltnW.

      by rewrite /pa /paS apegS -apegD [k + _]addnC.

    have P7 :
      (S_[b] n.+1).*2
      \sum_(i < b) `d[↓[u (inord (a + i))], ↓[u (inord (a + i).+1)]]_smove +
      sp ↓[u (inord a)] b pa + sp ↓[u (inord a1)] b (a[p1, p3] a1).

      apply: leq_trans (IH _ _ _ _ _ _ cH7) (leq_add (leq_add _ _) _);
        rewrite /pa /paS // 1?eq_sym //.

      - by rewrite apegS apeg_eqC eq_sym.

      - apply: leq_sumi; rewrite !ffunE !inordK ?addnS //.

          by rewrite ltnS.

        by rewrite ltnS ltnW.

      - by apply: leq_sumi _; rewrite !ffunE addn0.

      apply: leq_sumi _; rewrite !ffunE /= [a + b]addnC subnK //.

      by rewrite apegS -apegD subnK.

    set x4S := sp _ _ _ in P7; set y4S := sp _ _ _ in P7.

    have y3Sx4SE : y3S + x4S (S_[1] n).*2 + α_[maxn 2 b] n.

      apply: sum_alpha_diffE ⇒ //; first by rewrite /pa eq_sym.

      apply: codom_liftr.

      have := @cH (inord a); rewrite inordK //; apply.

      by rewrite a_gt0 /= ltnS (leq_trans _ a1Ll).

    rewrite (maxn_idPr _) // in y3Sx4SE.

    pose u5 := [ffun i : 'I_3
                     if i == 0 :> nat then ↓[u (inord a1)]
                 else if i == 1 :> nat then sa1 else ta1].

    have cH8 (k : 'I_3) :
      0 < k < 2 codom (u5 k) \subset [:: p1; a[p2, p3] k].

      move⇒ /andP[k_gt0 k_lt2].

      rewrite !ffunE.

      by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 ⇒ // [] [|].

    have P8 :
      (S_[2] n.+1).*2
      (`d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove) +
        sp ↓[u (inord a1)] 2 p2 + sp ta1 2 p2.

      apply: (leq_trans (IH _ _ _ _ _ _ cH8)) ⇒ //; first by rewrite eq_sym.

      repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.

      - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=.

      - by apply: eq_bigri _; rewrite !ffunE.

      by apply: eq_bigri _; rewrite !ffunE.

    set x5S := sp _ _ _ in P8; set y5S := sp _ _ _ in P8.

    have y4Sx5SE : y4S + x5S (S_[1] n).*2 + α_[maxn b 2] n.

      apply: sum_alpha_diffE ⇒ //.

      apply: codom_liftr; rewrite codom_subC.

      have := @cH (inord a1); rewrite inordK //.

        by apply; rewrite a1_gt0 /= ltnS.

      by rewrite ltnS ltnW.

    rewrite (maxn_idPl _) // in y4Sx5SE.

    have y2Sy5SE : y2S + y5S (S_[1] n).*2 + α_[maxn (3 × c).-2 2] n.

      apply: sum_alpha_diffE ⇒ //; first by rewrite /pa1.

      by rewrite codom_subC.

    rewrite (maxn_idPl _) // in y2Sy5SE.

    rewrite (_ : sd u =
       \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove +
       \sum_(a i < a1) `d[u (inord i), u (inord i.+1)]_smove +
       \sum_(a1 i < l.+1) `d[u (inord i), u (inord i.+1)]_smove); last first.

      pose f i := `d[u (inord i), u (inord i.+1)]_smove.

      rewrite /sd -!(big_mkord xpredT f).

      by rewrite -!big_cat_nat //= ltnW.

    rewrite -{}P1 -{}P2.

    rewrite [X in _ _ + X + _ + _ + _ + _]
       (_ : _ =
              \sum_(i < (3 × a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove
              + `d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove);
              last first.

      pose f i := `d[u1 (inord i), u1 (inord i.+1)]_smove.

      rewrite /sd -!(big_mkord xpredT f) .

      rewrite -{1}(subnK (_ : 1 < 3 × a)) //; last first.

        by rewrite -[a]prednK // mulnS.

      rewrite subn2 !addn2 !big_nat_recr /f //=; congr (_ + _ + _).

        rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.

          by rewrite -{1}[a]prednK // mulnS.

        rewrite inordK; last by rewrite ltnS ltn_mul2l /= prednK.

        rewrite mod3E /= eqxx.

        rewrite ffunE inordK; last first.

          by rewrite -[_.+3](mulnDr 3 1) add1n prednK // ltnW.

        by rewrite mod3E /= eqxx.

      rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.

        by rewrite -{1}[a]prednK // mulnS.

      rewrite inordK; last first.

        by rewrite -{2}[a]prednK // mulnS.

      rewrite mod3E /= eqxx.

      rewrite ffunE inordK; last first.

        by rewrite -{2}[a]prednK // mulnS.

      by rewrite -[(_ × _).+3](mulnDr 3 1) mod3E /= div3E add1n prednK.

    rewrite [X in _ _ + (_ + X) + _ + _]
       (_ : _ = `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove +
         \sum_(i < (3 × c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove);
        last first.

      pose f i := `d[u2 (inord i), u2 (inord i.+1)]_smove.

      rewrite /sd -!(big_mkord xpredT f) .

      rewrite -{1}(subnK (_ : 1 < 3 × c)) //; last first.

        by rewrite -[c]prednK // mulnS.

      rewrite subn2 !addn2 !big_nat_recl // /f /= !addnA; congr (_ + _ + _).

      - rewrite !ffunE !inordK ?addn0 //=.

        by rewrite ltnS muln_gt0.

      - rewrite !ffunE !inordK //=.

          by rewrite ltnW // ltnS (leq_mul2l 3 1 c).

        by rewrite ltnS muln_gt0.

      by rewrite big_mkord.

    rewrite -/y1S.

    set z1S := \sum_(_ < _) _; set z2S := \sum_(_ < _) _.

    set z3S := \sum_(_ _ < _) _.

    rewrite -/z1S in P4; rewrite -/z2S in P5; rewrite -/z3S in P3.

    rewrite -[z1S + _ + _]addnA; set d1 := `d[_,_]_ _ + `d[_,_]_ _;
       rewrite -/d1 in P6.

    set d2 := `d[_,_]_ _ + `d[_,_]_ _; rewrite -/d2 in P8.

    set xS := \sum_(_ _ < _) _ in P3.

    rewrite [X in _ X + _ + _](_ : _ = xS) in P7; last first.

      rewrite /xS -[in RHS](add0n a) big_addn -/b big_mkord.

      by apply: eq_bigri _; rewrite [a + _]addnC.

    have F1 := dsum_alphaL_S (3 × a).-2 n.

    have F2 := dsum_alphaL_S (3 × c).-2 n.

    have F3 := dsum_alphaL_S b n.

    have F4_a : 2 × a = 2 + a.-1 + a.-1.

      by rewrite -{1}[a]prednK // mul2n -addnn addnS.

    have F4_c : 2 × c = 2 + c.-1 + c.-1.

      by rewrite -{1}[c]prednK // mul2n -addnn addnS.

    have F4 i k : 0 < i S_[i.-1] k.+1 S_[(3 ×i).-2] k + i.-1.

      movei_gt0; apply: leq_trans (dsum_alpha3l _ _) _.

      rewrite leq_add2r.

      apply: (increasingE (increasing_dsum_alphaL_l _)).

      by rewrite -{2}[i]prednK // mulnS addSn add2n /=.

    have F4an := F4 a n a_gt0.

    have F4an1 := F4 a n.+1 a_gt0.

    have F4cn := F4 c n (c_gt0).

    have F4cn1 := F4 c n.+1 (c_gt0).

    have l_gt1 : 1 < l.

      by rewrite -ltnS l1E -[3]/(2 + 0 + 1); rewrite !leq_add.

    have F5 := SH l_gt1.

    have F6 : S_[l.+1] n.+2 + S_[1] n.+2 S_[a.-1] n.+2 + S_[(b + c).+2] n.+2.

      rewrite [X in _ X]addnC.

      rewrite (_ : l.+1 = 1 + a.-2 + (b + c).+1); last first.

        rewrite /b /c add1n -addSnnS !prednK //; last by rewrite -ltnS prednK.

        by rewrite addnCA addnA subnK // addnC subnK // ltnW.

      rewrite (_ : a.-1 = 1 + a.-2); last first.

         by rewrite add1n prednK // -ltnS prednK.

      by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).

    have F7 : S_[l] n.+1 + S_[1] n.+1 S_[a.-1] n.+1 + S_[(b + c).+1] n.+1.

      rewrite [X in _ X]addnC.

      rewrite (_ : l = 1 + a.-2 + (b + c)); last first.

        rewrite /b /c subSn // addnS -addSnnS add1n.

        rewrite !prednK //; last by rewrite -ltnS prednK.

        by rewrite addnCA addnA subnK // addnC subnK // ltnW.

      rewrite (_ : a.-1 = 1 + a.-2); last first.

         by rewrite add1n prednK // -ltnS prednK.

      by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).

    have F8 : S_[(b + c).+2] n.+2 + S_[1] n.+2 S_[c.-1] n.+2 + S_[b.+4] n.+2.

      rewrite (_ : (b + c).+2 = 1 + b.+3 + (c.-2)); last first.

        by rewrite add1n 2!addSnnS !prednK // -subn1 ltn_subRL addn0.

      rewrite (_ : c.-1 = 1 + c.-2); last first.

        by rewrite add1n prednK // -ltnS prednK.

      by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).

    have F9 : S_[(b + c).+1] n.+1 + S_[1] n.+1 S_[c.-1] n.+1 + S_[b.+3] n.+1.

      rewrite (_ : (b + c).+1 = 1 + b.+2 + (c.-2)); last first.

        by rewrite add1n 2!addSnnS !prednK // -subn1 ltn_subRL addn0.

      rewrite (_ : c.-1 = 1 + c.-2); last first.

        by rewrite add1n prednK // -ltnS prednK.

      by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).

    have F10 : S_[b.+4] n.+2 S_[b.+3] n.+1 + (α_[1] n.+1).*2.

      by apply: dsum_alphaL_alpha.

    have F11 : S_[b.+3] n.+1 S_[b.+2] n + (α_[1] n).*2.

      by apply: dsum_alphaL_alpha.

    have F12 : S_[b.+2] n + S_[1] n S_[b] n + S_[3] n.

      rewrite (_ : b.+2 = 1 + 2 + b.-1); last first.

        by rewrite add1n addSnnS prednK // ltnW.

      rewrite -{2}[b]prednK; last by apply: ltnW.

      by apply: concaveEk1 (concave_dsum_alphaL_l n).

    have F13 : S_[1] n.+1 = (S_[3] n).+1 by rewrite dsum_alpha3_S.

    have F14 := leq_dsum_alpha_2l_1 n.+1.

    have F15n := dsum_alphaL_S 1 n.+1.

    have F15n1 := dsum_alphaL_S 1 n.

    move: P3 P4 P5 P6 P7 P8P3 P4 P5 P6 P7 P8.

    applyr P3.

    rewrite -(leq_add2r x2S); applyr P4.

    rewrite -(leq_add2r y2S); applyr P5.

    rewrite -(leq_add2r (x3S + y3S)); applyr P6.

    rewrite -(leq_add2r (x4S + y4S)); applyr P7.

    rewrite -(leq_add2r (x5S + y5S)); applyr P8.

    applyl y4Sx5SE; applyl y3Sx4SE; applyl y2Sy5SE; applyl x2Sx3SE.

    gsimpl.

    rewrite ![2 × S_[_.-2] _]mul2n -!addnn {1}F1 {1}F2.

    rewrite {F1 F2}F3; gsimpl.

    rewrite {}F4_a {}F4_c.

    applyr F4an; applyr F4an1; applyr F4cn; applyr F4cn1.

    applyl F5.

    rewrite -(leq_add2r (S_[1] n.+2)); applyl F6.

    rewrite -(leq_add2r (S_[1] n.+1)); applyl F7.

    rewrite -(leq_add2r (S_[1] n.+2)); applyl F8.

    rewrite -(leq_add2r (S_[1] n.+1)); applyl F9; gsimpl.

    applyl F10.

    changel ((4 × S_[1] n + (α_[1] n.+1).*2 + S_[b.+3] n.+1).*2).

    changer ((2 + S_[2] n.+1 + S_[b] n + S_[2] n.+1 + S_[1] n.+2 +
      (S_[1] n.+1)).*2).

    rewrite leq_double.

    applyl F11; applyl F12; gsimpl; applyr F14.

    rewrite -ltnS -!addnS -F13.

    by rewrite {}F15n {}F15n1; gsimpl.

  move: b_le2; rewrite leq_eqVlt ⇒ /orP[/eqP[] bE1|].

    have a1E : a1 = a.+1 by rewrite -(subnK aLa1) -/b bE1.

    pose u3 := [ffun i : 'I_4
                 if i == 0 :> nat then sam1
                 else if i == 1 :> nat then tam1
                 else if i == 2 :> nat then ↓[u (inord a)]
                 else ↓[u (inord a.+1)]].

    have cH6 (k : 'I_4) :
      0 < k < 3 codom (u3 k) \subset [:: pa1S; a[p2, pa1] k].

      move⇒ /andP[k_gt0 k_lt3].

      rewrite !ffunE eqn_leq leqNgt k_gt0 /=.

      case: eqP ⇒ [->/=|/eqP kD1].

        by rewrite /pa1S !apegS apeg0 codom_apeg codom_subC.

      have ->/= : k = 2 :> nat.

        by apply/eqP; rewrite eqn_leq -ltnS k_lt3 ltn_neqAle eq_sym k_gt0 kD1.

      apply: codom_liftr; rewrite codom_subC.

      have /cH : 0 < (inord a : 'I_l.+2) < l.+1.

        rewrite inordK //.

        by rewrite a_gt0 /= l1E bE1 addn1 leq_addr.

      by rewrite inordK // /pa1S a1E !apegS apeg0.

    have P6 :
      (S_[3] n.+1).*2
      (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove +
          `d[↓[u (inord a)], ↓[u (inord a.+1)]]_smove) +
      sp sam1 3 p2 + sp ↓[u (inord a.+1)] 3 (a[p1, p3] a1).

      apply: (leq_trans (IH _ _ _ _ _ _ cH6)); rewrite /pa1S /pa1 //.

      - by rewrite eq_sym.

      - by rewrite eq_sym.

      - by rewrite apegS apeg_eqC eq_sym.

      repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.

      - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=.

      - by apply: eq_bigri _; rewrite !ffunE /=.

      by apply: eq_bigri _; rewrite !ffunE.

    set x3S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6.

    have x2Sx3SE : x2S + x3S (S_[1] n).*2 + α_[maxn (3 × a).-2 3] n.

      by apply: sum_alpha_diffE; rewrite /pa.

    rewrite (maxn_idPl _) in x2Sx3SE; last first.

      by rewrite -subn2 ltn_subRL ltnW // (leq_mul2l 3 2).

    pose u5 := [ffun i : 'I_3
                     if i == 0 :> nat then ↓[u (inord a1)]
                 else if i == 1 :> nat then sa1 else ta1].

    have cH8 (k : 'I_3) :
      0 < k < 2 codom (u5 k) \subset [:: p1; a[p2, p3] k].

      move⇒ /andP[k_gt0 k_lt2].

      rewrite !ffunE.

      by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 ⇒ // [] [|].

    have P8 :
      (S_[2] n.+1).*2
      (`d[↓[u (inord a.+1)], sa1]_smove + `d[sa1, ta1]_smove) +
      sp ↓[u (inord a.+1)] 2 p2 + sp ta1 2 p2.

      apply: (leq_trans (IH _ _ _ _ _ _ cH8)) ⇒ //.

        by rewrite eq_sym.

      repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.

      - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK //= a1E.

      - by apply: eq_bigri _; rewrite !ffunE a1E.

      by apply: eq_bigri _; rewrite !ffunE.

    set x5S := sp _ _ _ in P8; set y5S := sp _ _ _ in P8.

    have y3Sx5SE : y3S + x5S (S_[1] n).*2 + α_[3] n.

      apply: sum_alpha_diffE ⇒ //.

      apply: codom_liftr; rewrite codom_subC.

      have := @cH (inord a.+1); rewrite inordK ?a1E //.

        by apply; rewrite andTb //= ltnS -a1E.

      by rewrite -a1E ltnS ltnW.

    have y5Sy2SE : y5S + y2S (S_[1] n).*2 + α_[maxn 2 (3 × c).-2] n.

      by apply: sum_alpha_diffE; rewrite // /pa1 eq_sym.

    rewrite (maxn_idPr _) in y5Sy2SE; last first.

      by rewrite -subn2 ltn_subRL (ltn_mul2l 3 1).

    rewrite (_ : sd u =
       \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove +
       \sum_(a i < a1) `d[u (inord i), u (inord i.+1)]_smove +
       \sum_(a1 i < l.+1) `d[u (inord i), u (inord i.+1)]_smove);
        last first.

      pose f i := `d[u (inord i), u (inord i.+1)]_smove.

      rewrite /sd -!(big_mkord xpredT f).

      by rewrite -!big_cat_nat //= ltnW.

    rewrite -{}P1 -{}P2; applyr P3.

    rewrite (_ : sd u1 =
              \sum_(i < (3 × a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove
              + `d[sam1, tam1]_smove +
              `d[tam1, ↓[u (inord a)]]_smove); last first.

      pose f i := `d[u1 (inord i), u1 (inord i.+1)]_smove.

      rewrite /sd -!(big_mkord xpredT f) .

      rewrite -{1}(subnK (_ : 1 < 3 × a)) //; last first.

        by rewrite -[a]prednK // mulnS.

      rewrite subn2 !addn2 !big_nat_recr /f //=; congr (_ + _ + _).

        rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.

          by rewrite -{1}[a]prednK // mulnS.

        rewrite inordK; last by rewrite ltnS ltn_mul2l /= prednK.

        rewrite mod3E /= eqxx.

        rewrite ffunE inordK; last first.

          by rewrite -[_.+3](mulnDr 3 1) add1n prednK // ltnW.

        by rewrite mod3E /= eqxx.

      rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.

        by rewrite -{1}[a]prednK // mulnS.

      rewrite inordK; last first.

        by rewrite -{2}[a]prednK // mulnS.

      rewrite mod3E /= eqxx.

      rewrite ffunE inordK; last first.

        by rewrite -{2}[a]prednK // mulnS.

      by rewrite -[(_ × _).+3](mulnDr 3 1) mod3E /= div3E add1n prednK.

    rewrite (_ : sd u2 =
       `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove +
               \sum_(i < (3 × c).-2)
                  `d[u2 (inord i.+2), u2 (inord i.+3)]_smove); last first.

      pose f i := `d[u2 (inord i), u2 (inord i.+1)]_smove.

      rewrite /sd -!(big_mkord xpredT f) .

      rewrite -{1}(subnK (_ : 1 < 3 × c)) //; last first.

        by rewrite -[c]prednK // mulnS.

      rewrite subn2 !addn2 !big_nat_recl // /f /= !addnA.

       congr (_ + _ + _).

      - rewrite !ffunE !inordK ?addn0 //=.

        by rewrite ltnS muln_gt0.

      - rewrite !ffunE !inordK //=.

          by rewrite ltnW // ltnS (leq_mul2l 3 1 c).

        by rewrite ltnS muln_gt0.

      by rewrite big_mkord.

    rewrite (_ : \sum_(_ _ < _) _ =
      `d[↓[u (inord a)], ↓[u (inord a.+1)]]_smove); last first.

      by rewrite a1E big_nat1.

    set z1S := \sum_(_ < _) _ in P4; set z2S := \sum_(_ < _) _ in P5.

    rewrite -/z1S -/z2S.

    rewrite -a1E in P8; set d2 := `d[_,_]_ _ + `d[_,_]_ _ in P8; rewrite -/d2.

    set d1 := `d[_,_]_ _ + `d[_,_]_ _ + `d[_,_]_ _ in P6.

    rewrite -/y1S.

    changer (2 × a + 2 × c + x1S + y1S + z1S + z2S + d2 +
              (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove +
               `d[↓[u (inord a)], ↓[u (inord a.+1)]]_smove)).

    rewrite -/d1.

    have F1 := dsum_alphaL_S (3 × a).-2 n.

    have F2 := dsum_alphaL_S (3 × c).-2 n.

    have F3 := dsum_alphaL_S 3 n.

    have F4_a : 2 × a = 2 + a.-1 + a.-1.

      by rewrite -{1}[a]prednK // mul2n -addnn addnS.

    have F4_c : 2 × c = 2 + c.-1 + c.-1.

      by rewrite -{1}[c]prednK // mul2n -addnn addnS.

    have F4 i k : 0 < i S_[i.-1] k.+1 S_[(3 ×i).-2] k + i.-1.

      movei_gt0; apply: leq_trans (dsum_alpha3l _ _) _.

      rewrite leq_add2r.

      apply: (increasingE (increasing_dsum_alphaL_l _)).

      by rewrite -{2}[i]prednK // mulnS addSn add2n /=.

    have F4an := F4 a n a_gt0.

    have F4an1 := F4 a n.+1 a_gt0.

    have F4cn := F4 c n (c_gt0).

    have F4cn1 := F4 c n.+1 (c_gt0).

    have l_gt1 : 1 < l.

      by rewrite -ltnS l1E -[3]/(2 + 0 + 1); rewrite !leq_add.

    have F5 := SH l_gt1.

    have F6n : S_[1] n.+1 = (S_[3] n).+1 by rewrite dsum_alpha3_S.

    have F6n1 : S_[1] n.+2 = (S_[3] n.+1).+1 by rewrite dsum_alpha3_S.

    have am1_gt0 : 0 < a.-1 by rewrite -subn1 ltn_subRL addn0.

    have F7n1 : S_[1] n.+2 + S_[l.+1] n.+2 S_[a.-1] n.+2 + S_[c.+3] n.+2.

      rewrite addnC (_ : l.+1 = 1 + c.+2 + a.-2); last first.

        by rewrite /c a1E add1n !addSnnS !prednK ?subnK // -a1E ltnW.

      rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK.

      by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).

    have F7n : S_[1] n.+1 + S_[l] n.+1 S_[a.-1] n.+1 + S_[c.+2] n.+1.

      rewrite addnC (_ : l = 1 + c.+1 + a.-2); last first.

        by rewrite /c a1E add1n subSS !addSnnS !prednK ?subnK // -ltnS -a1E ltnW.

      rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK.

      by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).

    have cm1_gt0 : 0 < c.-1 by rewrite -subn1 ltn_subRL addn0.

    have F8n1 : S_[1] n.+2 + S_[c.+3] n.+2 S_[c.-1] n.+2 + S_[5] n.+2.

      rewrite addnC (_ : c.+3 = 1 + 4 + c.-2); last first.

        by rewrite add1n 2!addSnnS !prednK.

      rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK.

      by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).

    have F8n : S_[1] n.+1 + S_[c.+2] n.+1 S_[c.-1] n.+1 + S_[4] n.+1.

      rewrite addnC (_ : c.+2 = 1 + 3 + c.-2); last first.

        by rewrite add1n 2!addSnnS !prednK.

      rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK.

      by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).

    have F9 : S_[5] n.+2 S_[4] n.+1 + (α_[1] n.+1).*2.

      by apply: dsum_alphaL_alpha.

    have F10 : S_[4] n.+1 S_[3] n + (α_[1] n).*2.

      by apply: dsum_alphaL_alpha.

    have F11 : S_[1] n.+1 = (S_[3] n).+1 by rewrite dsum_alpha3_S.

    have F12 := leq_dsum_alpha_2l_1 n.+1.

    have F13n1 := dsum_alphaL_S 1 n.+1.

    have F13n := dsum_alphaL_S 1 n.

    move: P4 P5 P6 P8P4 P5 P6 P8.

    rewrite -(leq_add2r x2S); applyr P4.

    rewrite -(leq_add2r y2S); applyr P5.

    rewrite -(leq_add2r (x3S + y3S)); applyr P6.

    rewrite -(leq_add2r (x5S + y5S)); applyr P8.

    applyl y5Sy2SE; applyl y3Sx5SE; applyl x2Sx3SE.

    rewrite [2 × (S_[_.-2] _)]mul2n -addnn {1}F1.

    rewrite [2 × (S_[_.-2] _)]mul2n -addnn {1}F2.

    rewrite [2 × (S_[3] _)]mul2n -addnn {1}F3.

    gsimpl.

    rewrite {}F4_a {}F4_c.

    applyr F4an; applyr F4an1; applyr F4cn; applyr F4cn1.

    applyl F5.

    rewrite -ltnS -!addSn -!addnA [X in _ X]addnC !addnA -ltnS -!addSn.

    rewrite -{}F6n -{}F6n1.

    rewrite -(leq_add2r (S_[1] n.+2)); applyl F7n1.

    rewrite -(leq_add2r (S_[1] n.+1)); applyl F7n; gsimpl.

    rewrite -(leq_add2r (S_[1] n.+2)); applyl F8n1.

    rewrite -(leq_add2r (S_[1] n.+1)); applyl F8n; gsimpl.

    applyl F9.

    rewrite -leq_double in F10; applyl F10.

    rewrite -(leq_add2r 2).

    changel (6 × S_[1] n + 4 × α_[1] n.+1 + (α_[1] n).*2 + (α_[1] n).*2 +
      ((S_[3] n).+1).*2).

    rewrite -{}F11.

    applyr F12.

    by rewrite F13n1 F13n; gsimpl.

  rewrite !ltnS leqn0 ⇒ /eqP bE0.

  have a1E : a1 = a by rewrite -(subnK aLa1) -/b bE0.

  pose u3 := [ffun i : 'I_5
                 if i == 0 :> nat then sam1
                 else if i == 1 :> nat then tam1
                 else if i == 2 :> nat then ↓[u (inord a)]
                 else if i == 3 :> nat then sa1
                 else ta1].

  have cH6 (k : 'I_5) :
    0 < k < 4 codom (u3 k) \subset [:: pa1; a[p2, pa1S] k].

    move⇒ /andP[k_gt0 k_lt3].

    rewrite !ffunE eqn_leq leqNgt k_gt0 /=.

    case: eqP ⇒ [->/=|/eqP kD1].

      by rewrite /pa1S !apegS apeg0 codom_apeg.

    case: eqP =>[->/=|/eqP kD2].

      apply: codom_liftr; rewrite codom_subC.

      have /cH : 0 < (inord a : 'I_l.+2) < l.+1.

        by rewrite inordK // a_gt0 /= -a1E.

      by rewrite inordK // /pa1 a1E.

    have ->/= : k = 3 :> nat.

      by case: (k : nat) k_lt3 k_gt0 kD1 kD2 ⇒ // [] [|[|[|]]].

    by rewrite /pa1S !(apegS, apeg0) codom_apeg.

  have P6 :
    (S_[4] n.+1).*2
    (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove +
        `d[↓[u (inord a)], sa1]_smove +
        `d[sa1, ta1]_smove) + sp sam1 4 p2 + sp ta1 4 p2.

    apply: (leq_trans (IH _ _ _ _ _ _ cH6)); rewrite /pa1S /pa1 //.

    - by rewrite eq_sym.

    - by rewrite eq_sym.

    - by rewrite apegS apeg_eqC.

    repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.

    - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /= ?a1E.

    - by apply: eq_bigri _; rewrite !ffunE /=.

    by apply: eq_bigri _; rewrite !ffunE /= a1E.

  set x3S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6.

  have x2Sx3SE : x2S + x3S (S_[1] n).*2 + α_[maxn (3 × a).-2 4] n.

    by apply: sum_alpha_diffE; rewrite /pa.

  rewrite (maxn_idPl _) in x2Sx3SE; last first.

    by rewrite -subn2 ltn_subRL // (leq_mul2l 3 2).

  have y2Sy3SE : y2S + y3S (S_[1] n).*2 + α_[maxn (3 × c).-2 4] n.

    apply: sum_alpha_diffE ⇒ //; first by rewrite /pa1.

    by rewrite codom_subC.

  rewrite (maxn_idPl _) in y2Sy3SE; last first.

    by rewrite -subn2 ltn_subRL (leq_mul2l 3 2).

  rewrite (_ : sd u =
      \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove +
      \sum_(a1 i < l.+1) `d[u (inord i), u (inord i.+1)]_smove); last first.

    pose f i := `d[u (inord i), u (inord i.+1)]_smove.

    by rewrite /sd -!(big_mkord xpredT f) a1E -!big_cat_nat.

  rewrite -{}P1 -{P3}P2.

  rewrite (_ : sd u1 =
            \sum_(i < (3 × a).-2) `d[u1 (inord i), u1 (inord i.+1)]_smove
            + `d[sam1, tam1]_smove
            + `d[tam1, ↓[u (inord a)]]_smove); last first.

    pose f i := `d[u1 (inord i), u1 (inord i.+1)]_smove.

    rewrite /sd -!(big_mkord xpredT f) .

    rewrite -{1}(subnK (_ : 1 < 3 × a)) //; last first.

      by rewrite -[a]prednK // mulnS.

    rewrite subn2 !addn2 !big_nat_recr /f //=; congr (_ + _ + _).

      rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.

        by rewrite -{1}[a]prednK // mulnS.

      rewrite inordK; last by rewrite ltnS ltn_mul2l /= prednK.

      rewrite mod3E /= eqxx.

      rewrite ffunE inordK; last first.

        by rewrite -[_.+3](mulnDr 3 1) add1n prednK // ltnW.

      by rewrite mod3E /= eqxx.

    rewrite ffunE (_ : (3 × a).-2 = (3 × (a.-1)).+1); last first.

      by rewrite -{1}[a]prednK // mulnS.

    rewrite inordK; last first.

      by rewrite -{2}[a]prednK // mulnS.

    rewrite mod3E /= eqxx.

    rewrite ffunE inordK; last first.

      by rewrite -{2}[a]prednK // mulnS.

    by rewrite -[(_ × _).+3](mulnDr 3 1) mod3E /= div3E add1n prednK.

  rewrite [X in _ _ + (_ + X) + _ + _](_ : _ =
      `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove +
      \sum_(i < (3 × c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove);
       last first.

    pose f i := `d[u2 (inord i), u2 (inord i.+1)]_smove.

    rewrite /sd -!(big_mkord xpredT f) .

    rewrite -{1}(subnK (_ : 1 < 3 × c)) //; last first.

      by rewrite -[c]prednK // mulnS.

    rewrite subn2 !addn2 !big_nat_recl // /f /= !addnA; congr (_ + _ + _).

    - rewrite !ffunE !inordK ?addn0 //=.

      by rewrite ltnS muln_gt0.

    - rewrite !ffunE !inordK //=.

        by rewrite ltnW // ltnS (leq_mul2l 3 1 c).

      by rewrite ltnS muln_gt0.

    by rewrite big_mkord.

  set z1S := \sum_(_ < _) _ in P4; set z2S := \sum_(_ < _) _ in P5.

  rewrite -/z1S -/z2S.

  rewrite a1E -/y1S.

  changer (a.*2 + c.*2 + (`d[sam1, tam1]_smove + `d[tam1, ↓[u (inord a)]]_smove
    + `d[↓[u (inord a)], sa1]_smove + `d[sa1, ta1]_smove)
    + x1S + y1S + z1S + z2S).

  set d1 := `d[_,_]_ _ + `d[_,_]_ _ + `d[_,_]_ _ + `d[_,_]_ _;
    rewrite -/d1 in P6.

  have F1 := dsum_alphaL_S (3 × a).-2 n.

  have F2 := dsum_alphaL_S (3 × c).-2 n.

  have F3 := dsum_alphaL_S 4 n.

  have F4_a : 2 × a = 2 + a.-1 + a.-1.

    by rewrite mul2n -{1}[a]prednK // -addnn addnS.

  have F4_c : 2 × c = 2 + c.-1 + c.-1.

    by rewrite mul2n -{1}[c]prednK // -addnn addnS.

  have F4 i k : 0 < i S_[i.-1] k.+1 S_[(3 ×i).-2] k + i.-1.

    movei_gt0; apply: leq_trans (dsum_alpha3l _ _) _.

    rewrite leq_add2r.

    apply: (increasingE (increasing_dsum_alphaL_l _)).

    by rewrite -{2}[i]prednK // mulnS addSn add2n /=.

  have F4an := F4 a n a_gt0.

  have F4an1 := F4 a n.+1 a_gt0.

  have F4cn := F4 c n (c_gt0).

  have F4cn1 := F4 c n.+1 (c_gt0).

  have l_gt1 : 1 < l.

    by rewrite -ltnS l1E -[3]/(2 + 0 + 1); rewrite !leq_add.

  have F5 := SH l_gt1.

  have am1_gt0 : 0 < a.-1 by rewrite -subn1 ltn_subRL addn0.

  have F6n1 : S_[1] n.+2 + S_[l.+1] n.+2 S_[a.-1] n.+2 + S_[c.+2] n.+2.

    rewrite addnC (_ : l.+1 = 1 + c.+1 + a.-2); last first.

      by rewrite /c add1n 2!addSnnS !prednK ?a1E ?subnK.

    rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK.

    by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).

  have F6n : S_[1] n.+1 + S_[l] n.+1 S_[a.-1] n.+1 + S_[c.+1] n.+1.

    rewrite addnC (_ : l = 1 + c + a.-2); last first.

      rewrite /c add1n a1E -{1}[a]prednK // subSS.

      by rewrite !addSnnS !prednK // subnK // -ltnS prednK.

    rewrite {2}(_ : a.-1 = 1 + a.-2); last by rewrite add1n prednK.

    by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).

  have cm1_gt0 : 0 < c.-1 by rewrite -subn1 ltn_subRL addn0.

  have F7n1 : S_[1] n.+2 + S_[c.+2] n.+2 S_[c.-1] n.+2 + S_[4] n.+2.

    rewrite addnC (_ : c.+2 = 1 + 3 + c.-2); last first.

      by rewrite add1n 2!addSnnS !prednK.

    rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK.

    by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).

  have F7n : S_[1] n.+1 + S_[c.+1] n.+1 S_[c.-1] n.+1 + S_[3] n.+1.

    rewrite addnC (_ : c.+1 = 1 + 2 + c.-2); last first.

      by rewrite add1n 2!addSnnS !prednK.

    rewrite {2}(_ : c.-1 = 1 + c.-2); last by rewrite add1n prednK.

    by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).

  have F8 : S_[4] n.+2 S_[3] n.+1 + (α_[1] n.+1).*2.

    by apply: dsum_alphaL_alpha n.+1 (isT : 1 < 3).

  have F9 : S_[3] n.+1 S_[4] n.+1 by case: (concave_dsum_alphaL_l n.+1).

  have F10n1 := dsum_alphaL_S 1 n.+1.

  have F10n := dsum_alphaL_S 1 n.

  have F11 := bound_alphaL 2 n.

  have F12 := alphaL_1_2 n.

  move: P4 P5 P6P4 P5 P6.

  rewrite -(leq_add2r x2S); applyr P4.

  rewrite -(leq_add2r y2S); applyr P5.

  rewrite -(leq_add2r (x3S + y3S)); applyr P6.

  applyl x2Sx3SE; applyl y2Sy3SE; gsimpl.

  rewrite [2 × (S_[_.-2] _)]mul2n -addnn {1}F1.

  rewrite [2 × (S_[_.-2] _)]mul2n -addnn {1}F2.

  gsimpl.

  rewrite {}F4_a {}F4_c.

  applyr F4an1; applyr F4an; applyr F4cn1; applyr F4cn.

  applyl F5.

  rewrite -(leq_add2r (S_[c.+2] n.+2)); applyr F6n1.

  rewrite -(leq_add2r (S_[c.+1] n.+1)); applyr F6n; gsimpl.

  rewrite -(leq_add2r (S_[1] n.+2)); applyl F7n1.

  rewrite -(leq_add2r (S_[1] n.+1)); applyl F7n.

  applyl F8; gsimpl.

  changel ((α_[1] n.+1).*2 + (S_[1] n).*2 + (S_[1] n).*2 +
    (α_[1] n.+1).*2 + (S_[3] n.+1).*2).

  changer (4 + S_[1] n.+2 + S_[1] n.+1 + S_[1] n.+2 + S_[1] n.+1 +
    (S_[4] n.+1).*2).

  apply: leq_add; last by rewrite leq_double.

  rewrite F10n1 F10n; gsimpl.

  by rewrite -leq_double in F12; applyl F12; gsimpl.

rewrite negb_and -!leqNgtacH.

have aLc : a c by [].

have aE1 : a = 1.

  case/orP: acH; case: (a) aLc a_gt0 ⇒ // [] [|n1] //.

  by case: (c) ⇒ // [] [].

have leq_S4 k : 5 × S_[1] k.+1 + S_[1] k.+2 6 × S_[4] k + 9.

  have F3 : 4 × S_[3] k + 2 × S_[6] k 6 × S_[4] k.

    rewrite -{1}[4]/(2 × 2) -mulnA -mulnDr -{2}[6]/(2 × 3) -mulnA.

    rewrite leq_mul2l /= -(leq_add2r (S_[5] k)).

    changel (S_[6] k + S_[3] k + (S_[5] k + S_[3] k)).

    changer (S_[5] k + S_[4] k + (S_[4] k + S_[4] k)).

    by apply: leq_add; apply: concaveEk1 3 _ _ (concave_dsum_alphaL_l k).

  applyr F3.

  have F3k : S_[1] k.+1 S_[3] k + 1 by apply: dsum_alpha3l.

  have F3k1 : S_[2] k.+1 S_[6] k + 2 by apply: dsum_alpha3l.

  rewrite -leq_double in F3k1; applyr F3k1.

  rewrite -2!leq_double in F3k; applyr F3k; gsimpl.

  by have F4 := leq_dsum_alpha_2l_1 k.+1; applyr F4.

move: c_gt0; rewrite leq_eqVlt eq_sym ⇒ /orP[/eqP cE1|c_gt1].

  move : P1 P2 P3P1 P2 P3.

  have l_gt0 : 0 < l by rewrite -ltnS l1E aE1 cE1 addn1.

  have a1El : a1 = l.

    by rewrite -(subKn (_ : a1 l.+1)) 1?ltnW // -/c cE1 subSS subn0.

  have [b_gt1|b_lt2]:= leqP 2 b.

    rewrite (_ : sd u =
        \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove +
        \sum_(a i < a1) `d[u (inord i), u (inord i.+1)]_smove +
        \sum_(a1 i < l.+1) `d[u (inord i), u (inord i.+1)]_smove);
        last first.

      pose f i := `d[u (inord i), u (inord i.+1)]_smove.

      rewrite /sd -!(big_mkord xpredT f).

      by rewrite -!big_cat_nat //= ltnW.

    rewrite !sum_beta_S // KH1 eqxx addn0 KH2 eqxx addn0.

    apply: leq_trans (leq_add (leq_add (leq_add (leq_add (leqnn _) P3)
                       (leqnn _)) (leqnn _)) (leqnn _)); rewrite -{P3}P1 -{}P2.

    set x2S := sd u2; set x0S := sd u1.

    pose u3 := [ffun i : 'I_b.+1 ↓[u (inord (a + i))]].

    rewrite (_ : \sum_(_ _ < _) _ =
        \sum_(i < b) `d[u3 (inord i), u3 (inord i.+1)]_smove); last first.

      rewrite -{1}[a]add0n big_addn -/b big_mkord.

      apply: eq_bigri _.

      by rewrite !ffunE addnC !inordK ?(addnS, ltnS) // ltnW.

    pose paS := a[p1, p3] a.+1.

    have cH3 (k : 'I_b.+1) :
      0 < k < b codom (u3 k) \subset [:: p2; a[pa, paS] k].

      move⇒ /andP[k_gt0 k_ltb].

      have akLl : a + k < l.+1.

        rewrite ltnS (leq_trans _ a1Ll) //.

        by rewrite -(subnK aLa1) addnC leq_add2r ltnW.

      rewrite !ffunE.

      have /H : 0 < (inord (a + k) : 'I_l.+2) < l.+1.

        rewrite inordK; first by rewrite addn_gt0 a_gt0.

        by rewrite ltnS ltnW.

      rewrite ffunE inordK //; last by rewrite ltnS ltnW.

      by rewrite /paS apegS -apegD [k + _]addnC.

    pose pa1 := a[p1, p3] a1.

    have P3 :
      (S_[b] n.+1).*2
      \sum_(i < b) `d[↓[u (inord (a + i))], ↓[u (inord (a + i).+1)]]_smove +
      sp ↓[u (inord a)] b pa + sp ↓[u (inord a1)] b pa1.

      apply: leq_trans (IH _ _ _ _ _ _ cH3) (leq_add (leq_add _ _) _);
        rewrite /pa /paS // 1?eq_sym //.

      - by rewrite apegS apeg_eqC eq_sym.

      - apply: leq_sumi; rewrite !ffunE !inordK ?addnS //.

          by rewrite ltnS.

        by rewrite ltnS ltnW.

      - by apply: leq_sumi _; rewrite !ffunE addn0.

      apply: leq_sumi _; rewrite !ffunE /= [a + b]addnC subnK //.

      by rewrite apegS -apegD subnK.

    set x1S := \sum_(_ < _) _ in P3; set y2S := sp _ _ _ in P3.

    set y3S := sp _ _ _ in P3.

    rewrite [\sum_(_ < _) _](_ : _ = x1S); last first.

      by apply: eq_bigri; rewrite !ffunE !inordK ?addnS // ltnS // ltnW.

    set y0S := \sum_(_ < _) _ ; set y5S := \sum_(_ < _) _.

    have cH1 (k : 'I_(3 × a).+1) :
      0 < k < 3 × a codom (u1 k) \subset [:: p3; a[p1, p2] k].

      move⇒ /andP[k_gt0 k_ltb].

      rewrite {2}aE1 muln1 in k_ltb.

      rewrite ffunE !modn_small // !divn_small // inord_eq0 //.

      rewrite [in 3 × a.-1]aE1 /=.

      case: (k : nat) k_gt0 k_ltb ⇒ //= [] [|[|]] //= _ _.

        rewrite !(apegS, apeg0).

        by have := sam1C; rewrite /pa aE1 apegS apeg0.

      by rewrite !(apegS, apeg0) codom_subC.

    have P1 :
      (S_[3 × a] n.+1).*2 x0S + sp ↓[u ord0] 3 p1 + sp ↓[u (inord a)] 3 p2.

      apply: leq_trans (IH _ _ _ _ _ _ cH1) (leq_add (leq_add _ _) _);
          rewrite // 1?eq_sym //.

        by apply: leq_sumi _; rewrite ffunE /= inord_eq0 // aE1 muln1.

      by apply: leq_sumi _; rewrite ffunE /= mod3E /= div3E // aE1 muln1.

    have {}P1 := leq_trans P1 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                          (leqnn _)).

    rewrite -/y0S in P1; set y1S := sp _ _ _ in P1.

    rewrite aE1 muln1 in P1.

    have y1Sy2SE : y1S + y2S (S_[1] n).*2 + α_[maxn 3 b] n.

      apply: sum_alpha_diffE ⇒ //; first by rewrite /pa // eq_sym.

      apply: codom_liftr.

      have /cH : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK.

      by rewrite /pa aE1 inordK.

    have cH2 (k : 'I_(3 × c).+1) :
      0 < k < 3 × c
      codom (u2 k) \subset [:: a[p1, p3] a1; a[p2, a[p1, p3] a1.+1] k].

      move⇒ /andP[k_gt0 k_ltb].

      rewrite {2}cE1 muln1 in k_ltb.

      rewrite ffunE !modn_small // !divn_small // addn0.

      case: (k : nat) k_gt0 k_ltb ⇒ //= [] [|[|]] //= _ _.

        by rewrite !apegS apeg0 codom_apeg.

      by rewrite !(apegS, apeg0) codom_subC.

    have P2 :
      (S_[3 × c] n.+1).*2 x2S + sp ↓[u (inord a1)] 3 p2 +
                             sp ↓[u ord_max] 3 (a[p3, p1] l).

      apply: leq_trans (IH _ _ _ _ _ _ cH2) (leq_add (leq_add _ _) _);
          rewrite // 1?eq_sym //.

      - by rewrite apegS apeg_eqC eq_sym.

      - by apply: leq_sumi _; rewrite ffunE /= addn0 cE1 muln1.

      apply: leq_sumi _; rewrite ffunE /= mod3E /= div3E // cE1 muln1.

      rewrite a1El addn1 (_ : inord _ = ord_max) ?apegS //.

      by apply/val_eqP; rewrite /= inordK.

    have {}P2 := leq_trans P2 (leq_add (leqnn _) (leq_sum_beta _ _)).

    rewrite -/y5S in P2; set y4S := sp _ _ _ in P2.

    have y3Sy4SE : y3S + y4S (S_[1] n).*2 + α_[maxn b 3] n.

      apply: sum_alpha_diffE; rewrite /pa /pa1 //.

      apply: codom_liftr; rewrite codom_subC.

      have /cH : 0 < (inord l : 'I_l.+2) < l.+1 by rewrite inordK // l_gt0 /=.

      by rewrite a1El inordK.

    have Eb1 : l = b.+1.

      by have := l1E; rewrite aE1 cE1 addn1 ⇒ [] [].

    rewrite Eb1.

    have F1b := dsum_alphaL_S b n.

    have F1n31 : (S_[3] n.+1).+1 = S_[1] n.+2.

      by rewrite dsum_alpha3_S.

    have F1n1 := dsum_alphaL_S 1 n.

    have F1n2 := dsum_alphaL_S 1 n.+1.

    have b_gt0 : 0 < b by apply: leq_trans b_gt1.

    have F2n1 : S_[b.+2] n.+2 S_[b.+1] n.+1 + (α_[1] n.+1).*2.

      by rewrite dsum_alphaL_alpha .

    have F2n : S_[b.+1] n.+1 S_[b] n + (α_[1] n).*2.

      by rewrite dsum_alphaL_alpha.

    have F3n : S_[4] n.+2 S_[3] n.+1 + (α_[1] n.+1).*2.

      by rewrite dsum_alphaL_alpha.

    have F4n := alphaL_3E n.

    have F5 := leq_dsum_alpha_2l_1 n.+1.

    move: P1 P2 P3P1 P2 P3.

    rewrite -(leq_add2r y1S); applyr P1.

    rewrite -(leq_add2r y4S); applyr P2.

    rewrite -(leq_add2r (y2S + y3S)); applyr P3.

    applyl y3Sy4SE; applyl y1Sy2SE; gsimpl.

    rewrite maxnC aE1 cE1 !muln1.

    changel ((S_[b.+2] n.+2 + (S_[1] n).*2 + α_[maxn 3 b] n).*2).

    changer (((S_[3] n.+1).+1.*2 + S_[b] n.+1).*2).

    rewrite leq_double.

    move: b_gt1; rewrite leq_eqVlt ⇒ /orP[/eqP<-|b_gt2]; last first.

      rewrite (maxn_idPr _) //.

      rewrite F1b addnA leq_add2r F1n31 F1n2 F1n1.

      by applyr F2n; applyr F2n1; gsimpl.

    rewrite (maxn_idPl _) //.

    applyl F3n; gsimpl.

    rewrite -ltnS -![in X in _ X]addSn !{}F1n31 {}F4n; gsimpl.

    rewrite F1n2; gsimpl.

    have [n_gt3 |] := leqP 4 n; last first.

      by case: n ⇒ [|[|[|[|n1]]]]; rewrite // !(alphaS_small, alpha_small).

    rewrite -leq_double; applyr F5.

    rewrite F1n2 F1n1; gsimpl.

    by have F := alpha_4_3 (n_gt3); applyr F.

  move: b_lt2; rewrite leq_eqVlt ⇒ /orP[/eqP [] bE1 | b_lt1].

    pose u1l :=
      [ffun i
        if (i : 'I_5) == 0 :> nat then ↓[u ord0] else
        if i == 1 :> nat then sam1 else
        if i == 2 :> nat then tam1 else
        if i == 3 :> nat then ↓[u (inord 1)] else ↓[u (inord 2)]].

    have a1E2 : a1 = 2.

      by move: (cE1); rewrite /c l1E aE1 bE1 cE1; case: (a1) ⇒ // [] [|[|]].

    have P1l1 : a.*2 + sd u1l
      \sum_(i < a1) `d[u (inord i), u (inord i.+1)]_smove.

      rewrite /sd a1E2 !big_ord_recr /= !big_ord0 !add0n {1}aE1.

      rewrite !ffunE /= !inordK ?aE1 //= add2n -2!addSn leq_add //; last first.

        by apply/gdist_cunlift/shanoi_connect.

      rewrite (inord_eq0 _ (_ : 0 = 0)) //.

      rewrite (_ : ord0 = inord a.-1); last first.

        by apply/val_eqP; rewrite /= inordK aE1.

      by rewrite -[in inord 1]aE1 duam1ua1E /= addnA addn0.

    have cH1 (k : 'I_5) :
      0 < k < 4 codom (u1l k) \subset [:: p3; a[p1, p2] k].

      case: k ⇒ [] [|[|[|[|]]]] //= iH _; rewrite !ffunE !(apegS, apeg0).

      - by have := sam1C; rewrite /pa aE1.

      - by rewrite codom_subC.

      apply: codom_liftr; rewrite codom_subC.

      have /cH: 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite inordK.

      by rewrite inordK.

    have lE2 : l = 2 by move: l1E; rewrite aE1 bE1 cE1 ⇒ [] [].

    have {cH1}P4 :
      (S_[4] n.+1).*2 sd u1l + sp ↓[u ord0] 4 p1 +
                                  sp ↓[u (inord a1)] 4 p1.

      apply: leq_trans (IH _ _ _ _ _ _ cH1) _ ⇒ //.

        by rewrite eq_sym.

      repeat apply: leq_add ⇒ //; apply: leq_sumi /= _; rewrite !ffunE //.

      by rewrite a1El -[in inord 2]lE2.

    have {}P4 := leq_trans P4 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                                    (leqnn _)).

    set x1S := sd _ in P4.

    set y1S := \sum_(_ < _) _ in P4; set y2S := sp _ _ _ in P4.

    have cH2 (k : 'I_(3 × c).+1) :
      0 < k < 3 × c
      codom (u2 k) \subset [:: a[p1, p3] a1; a[p2, a[p1, p3] a1.+1] k].

      move⇒ /andP[k_gt0 k_ltb].

      rewrite {2}cE1 muln1 in k_ltb.

      rewrite ffunE !modn_small // !divn_small // addn0.

      case: (k : nat) k_gt0 k_ltb ⇒ //= [] [|[|]] //= _ _.

        by rewrite a1E2.

      by rewrite codom_subC.

    have P5 :
      (S_[3 × c] n.+1).*2 sd u2 + sp ↓[u (inord a1)] 3 p2 +
                                     sp ↓[u ord_max] 3 (a[p3, p1] l).

      apply: leq_trans (IH _ _ _ _ _ _ cH2) (leq_add (leq_add _ _) _);
          rewrite // 1?eq_sym //.

      - by rewrite a1E2 eq_sym.

      - by apply: leq_sumi _; rewrite ffunE /= addn0 cE1 muln1.

      apply: leq_sumi _; rewrite ffunE /= mod3E /= div3E // cE1 muln1.

      rewrite a1El addn1 (_ : inord _ = ord_max) ?apegS //.

      by apply/val_eqP; rewrite /= inordK.

    have {}P5 := leq_trans P5 (leq_add (leqnn _) (leq_sum_beta _ _)).

    rewrite // {1}[in 3 ×c]cE1 muln1 in P5.

    set x2S := sd _ in P5.

    set y3S := sp _ _ _ in P5; set y4S := \sum_(_ < _) _ in P5.

    rewrite /sd -(big_mkord xpredT
                   (fun i`d[u (inord i), u (inord i.+1)]_smove)).

    rewrite (big_cat_nat _ _ _ (_ : 0 a1)) //=; last by apply: ltnW.

    rewrite big_mkord -!addnA.

    apply: leq_trans (leq_add P1l1 (leqnn _)); rewrite -/x1S.

    rewrite -{P1l1}P2 -/x2S {1}lE2 !sum_beta_S //.

    rewrite KH1 KH2 !eqxx !addn0 aE1 -/y1S -/y4S.

    have y2Sy3SE : y2S + y3S (S_[1] n).*2 + α_[4] n.

      apply: sum_alpha_diffE ⇒ //.

      apply: codom_liftr; rewrite codom_subC.

      have /cH : 0 < (inord a1 : 'I_l.+2) < l.+1 by rewrite inordK // a1E2 lE2.

      by rewrite inordK // a1E2.

    rewrite {1}aE1 -[1.*2]/2 in P1.

    rewrite {1}cE1 -[1.*2]/2.

    have F1n4 := dsum_alphaL_S 4 n.

    have F1n3 : (S_[3] n.+2).+1 = S_[1] n.+3.

      by rewrite -dsum_alpha3_S.

    have F1n13 : (S_[3] n.+1).+1 = S_[1] n.+2.

      by rewrite -dsum_alpha3_S.

    move: P4 P5P4 P5.

    rewrite -(leq_add2r y2S); applyr P4.

    rewrite -(leq_add2r y3S); applyr P5.

    applyl y2Sy3SE.

    rewrite [in X in _ X]mul2n -addnn.

    rewrite {1}F1n4; gsimpl.

    rewrite -(leq_add2r 2).

    changel (((S_[3] n.+2).+1).*2 + (S_[1] n).*2).

    changer (4 + S_[4] n + S_[4] n.+1 + ((S_[3] n.+1).+1).*2).

    rewrite {}F1n3 {}F1n13.

    case : n ⇒ [|[|[|[|n1]]]]; try by rewrite !alphaS_small.

    set m1 := n1.+3.

    rewrite -(leq_add2r (S_[1] m1.+2).*2).

    rewrite -[_ _](leq_mul2l 6).

    have F := leq_S4 m1.+1; applyr F.

    have F := leq_S4 m1.+2; applyr F; gsimpl.

    have F3n3 := dsum_alphaL_S 1 m1.+3.

    have F3n2 := dsum_alphaL_S 1 m1.+2.

    have F3n1 := dsum_alphaL_S 1 m1.+1.

    rewrite !(F3n3, F3n2, F3n1); gsimpl.

    have F4m1 : 12 × α_[1] m1.+3 16 × α_[1] m1.+2.

      rewrite -[12]/(4 × 3) -mulnA.

      rewrite -[16]/(4 × 4) -mulnA leq_mul2l /=.

      by rewrite alpha_4_3.

    apply: leq_trans (leq_trans _ F4m1) _; first by rewrite leq_mul2r orbT.

    gsimpl.

    have F4m2 : 9 × α_[1] m1.+2 12 × α_[1] m1.+1.

      rewrite -[12]/(3 × 4) -mulnA.

      rewrite -[9]/(3 × 3) -mulnA leq_mul2l /=.

      by rewrite alpha_4_3.

    by applyr F4m2; gsimpl.

  have bE0 : b = 0 by case: (b) b_lt1 ⇒ //.

  have lE1 : l = 1 by have := l1E; rewrite aE1 bE0 cE1 ⇒ [] [].

  have a1E1 : a1 = 1 by rewrite a1El.

  rewrite (_ : a[p3, p1] l = a[p2, p1] l); last by rewrite lE1.

  apply: (@case2 _ IH) ⇒ //.

  - by rewrite (_ : a[p1, p3] _ = a[p1, p3] 1).

  - movek hK; rewrite {3}lE1 in hK.

    have → : k = inord 1.

      apply/val_eqP; rewrite /= inordK //.

      by case: (k : nat) hK ⇒ [] // [|].

    rewrite inordK //= !(apegS, apeg0) //= codom_subC.

    have := cH (inord 1).

    rewrite inordK // !(apegS, apeg0).

    by apply.

  - by rewrite KH2 lE1.

  movek.

  have [->|[->|->]] // : k = ord0 k = (inord 1) k = (inord 2).

  - move: k; rewrite lE1.

    case ⇒ [] []; first by left; apply: val_inj ⇒ /=.

    case.

      by right; left; apply: val_inj; rewrite /= inordK.

    case ⇒ //.

    by right; right; apply: val_inj; rewrite /= inordK.

  by rewrite -[in inord 1]aE1 uaLEp2 aE1 inordK.

  rewrite {1}(_ : inord 2 = ord_max); last first.

    by apply/val_eqP; rewrite /= lE1 inordK.

  by rewrite KH2 lE1 /= inordK.

pose u2r := [ffun i : 'I_(3 × c).-2.+1 u2 (inord i.+2)].

pose pa1 := a[p1, p3] a1.

pose pa1S := a[p1, p3] a1.+1.

have cH8 (k : 'I_(3 × c).-2.+1) :
  0 < k < (3 × c).-2 codom (u2r k) \subset [:: p2; a[pa1, pa1S] k].

  move⇒ /andP[k_gt0 k3L3a].

  have k2L3c : k.+2 < (3 × c).

    by have := k3L3a; rewrite -{2}subn2 ltn_subRL add2n.

  rewrite !ffunE inordK ?ltnS 1?ltnW //.

  case: eqP ⇒ [km3E0 /= |/eqP km3D0].

    have k3_gt0 : 0 < k.+2 %/ 3.

      case: (k: nat) k_gt0 km3E0 ⇒ // [] //= k1 _ _.

      by rewrite (divnMDl 1 k1 (_ : 0 < 3)).

    have a1k3Ll1 : a1 + k.+2 %/ 3 < l.+1.

      move: k2L3c.

      rewrite {1}(divn_eq k.+2 3) km3E0 addn0 mulnC ltn_mul2l /= ⇒ k2L3c.

      rewrite -(subnK (_ : a1 l.+1)) ?(leq_trans a1Ll) //.

      by rewrite addnC ltn_add2r -/c.

    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first.

      by rewrite /pa1S !addnS !apegS -apegD addnC.

    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3)) ; last first.

      rewrite apegO oddD {1}(divn_eq k.+2 3) !oddD odd_mul andbT -oddD.

      by rewrite km3E0 addn0 -oddD -apegO.

    have /H : 0 < (inord (a1 + k.+2 %/ 3) : 'I_l.+2) < l.+1.

      rewrite inordK; first by rewrite addn_gt0 a1_gt0.

      by rewrite ltnS ltnW.

    by rewrite ffunE inordK // ltnS ltnW.

  case: eqP ⇒ [km3E1|/eqP km3D1].

    rewrite eqn_leq ltnNge /=.

    have a1La1k : a1 < a1 + k.+2 %/3.

      by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0.

    have a1k3Ll : a1 + k.+2 %/ 3 < l.+1.

      move: (ltnW k2L3c).

      rewrite {1}(divn_eq k.+2 3) km3E1 addn1 mulnC ltn_mul2l /=.

      rewrite -(subnK (_ : a1 l.+1)) ?(leq_trans a1Ll) //.

      by rewrite addnC ltn_add2r -/c.

    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first.

      by rewrite /pa1S !addnS !apegS -apegD addnC.

    rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3).+1) ; last first.

      rewrite apegS apegO {1}(divn_eq k.+2 3) !oddD odd_mul andbT.

      by rewrite km3E1 addbT addbN -oddD -oddS -apegO apegS.

    case: (sitiHb (a1 + k.+2 %/ 3)) ⇒ // [| siH _ _]; first by rewrite a1La1k.

    by move: siH; rewrite a1Max // ltnS ltnW.

  have km3E2 : k.+2 %% 3 = 2.

    by case: (_ %% _) (ltn_mod k.+2 3) km3D0 km3D1 ⇒ // [] [|[|]].

  rewrite ifN; last by case: (k : nat) k_gt0.

  have a1La1k : a1 < a1 + k.+2 %/3.

    by rewrite -{1}(addn0 a1) ltn_add2l divn_gt0.

  have a1k3Ll : a1 + k.+2 %/ 3 < l.+1.

    have: k.+2 %/ 3 × 3 < 3 × c.

      rewrite ltnW //.

      move: (ltnW k2L3c).

      by rewrite {1}(divn_eq k.+2 3) km3E2 addn2.

    rewrite mulnC ltn_mul2l /=.

    rewrite -(subnK (_ : a1 l.+1)) ?(leq_trans a1Ll) //.

    by rewrite addnC ltn_add2r -/c.

  rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + k.+2)) ; last first.

    by rewrite !addnS /pa1S !apegS -apegD addnC.

  rewrite (_ : a[_, _ ] _ = a[p1, p3] (a1 + (k.+2) %/ 3)) ; last first.

    rewrite apegO {1}(divn_eq k.+2 3) !oddD odd_mul andbT.

    by rewrite km3E2 addbF -oddD -apegO.

  rewrite codom_subC.

  case: (sitiHb (a1 + k.+2 %/ 3)) ⇒ // [| _ tiH _]; first by rewrite a1La1k.

  by move: tiH; rewrite a1Max // a1La1k ltnS ltnW.

have c_gt0 : 0 < c by rewrite ltnW.

have P8 :
  (S_[(3 × c).-2] n.+1).*2
  \sum_(i < (3 × c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove +
  sp ta1 (3 × c).-2 pa1 + sp ↓[u ord_max] (3 × c).-2 (a[p3, p1] l).

  apply: leq_trans (IH _ _ _ _ _ _ cH8) _; rewrite /pa1 /pa1S {cH8}//.

  - by rewrite apegS apeg_eqC.

  - by rewrite eq_sym.

  repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.

  - apply: eq_bigri _.

    by rewrite ![u2r _]ffunE !inordK // ltnS // ltnW.

  - apply: eq_bigri _; congr ((_ != _) × _).

    rewrite !ffunE /= !inordK //=.

    by rewrite (leq_trans (_ : 2 < (3 × 1).+1)) // ltnS leq_mul2l ltnW.

  apply: eq_bigri _; congr ((_ != _) × _).

    rewrite !ffunE /= !prednK ?muln_gt0 //=; last first.

      by rewrite -subn1 ltn_subRL addn0 (leq_trans (_ : _ < 3 × 1)) //
                 leq_mul2l.

    rewrite inordK // mod3E /= div3E addnC subnK; last first.

      by apply: (leq_trans a1Ll).

    by rewrite ffunE; congr (u _ _ ); apply/val_eqP; rewrite /= inordK.

  rewrite /pa1 /pa1S -[RHS]apegS -(subnK (_ : a1 l.+1)) // -/c.

    rewrite apegS -apegD apegO -subn2 oddD oddB //.

      by rewrite odd_mul /= addbF -oddD -apegO.

    by rewrite (leq_trans (_ : _ < 3 × 1)) // leq_mul2l //.

  by rewrite ltnW.

rewrite {cH8}//.

have l_gt0 : 0 < l.

  by rewrite -ltnS l1E aE1 add1n addSn ltnS addn_gt0 c_gt0 orbT.

have c3m2_gt1 : 1 < (3 × c).-2.

  by rewrite -subn2 ltn_subRL -[2 +1]/(3 × 1) ltn_mul2l.

have {}P8 := leq_trans P8 (leq_add (leq_add (leqnn _) (leqnn _))
                      (leq_sum_beta _ _)).

set y7S := sp _ _ _ in P8; set y8S := \sum_(_ < n.+1) _ in P8.

rewrite !sum_beta_S // KH1 KH2 !eqxx !addn0 -/y8S.

rewrite (_ : sd u =
  \sum_(i < a) `d[u (inord i), u (inord i.+1)]_smove +
  \sum_(a i < a1) `d[u (inord i), u (inord i.+1)]_smove +
  \sum_(a1 i < l.+1) `d[u (inord i), u (inord i.+1)]_smove); last first.

  rewrite /sd -[X in _ = X + _ + _](big_mkord xpredT
                (fun i`d[u (inord i), u (inord i.+1)]_smove)).

  by rewrite -!big_cat_nat ?big_mkord //= ltnW.

rewrite -{}P1 -{}P2.

move: P3P3.

rewrite -2!addnA.

apply: leq_trans (leq_add (leq_add (leqnn _) P3) (leqnn _)); rewrite {P3}//.

have du2E : `d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove =
             \sum_(i < 2) `d[u2 (inord i), u2 (inord i.+1)]_smove.

  rewrite !big_ord_recr /= big_ord0 !ffunE !inordK //= ?addn0 //.

    by rewrite ltnW // ltnS (leq_mul2l 3 1).

  by rewrite ltnS muln_gt0.

rewrite (_ : sd u2 =
  (`d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove) +
  \sum_(i < (3 × c).-2) `d[u2 (inord i.+2), u2 (inord i.+3)]_smove);
   last first.

  rewrite /sd du2E.

  rewrite -!(big_mkord xpredT
                (fun i`d[u2 (inord i), u2 (inord i.+1)]_smove)).

  rewrite -!(big_mkord xpredT
                (fun i`d[u2 (inord i.+2), u2 (inord i.+3)]_smove)).

  rewrite[X in _ = _ + X] (eq_bigr
                (fun i`d[u2 (inord (i + 2)), u2 (inord (i + 2).+1)]_smove));
    last by movei_; rewrite !addn2.

  rewrite -subn2.

  have <- := big_addn _ _ _ xpredT
               (fun i`d[u2 (inord i), u2 (inord i.+1)]_smove).

  rewrite -big_cat_nat //.

  by rewrite ltnW // (leq_mul2l 3 1).

set x3S := \sum_(_ < _) _ in P8; rewrite -/x3S.

have [|b_gt0] := leqP b 0; last first.

  have cH1 (k : 'I_(3 × a).+1) :
    0 < k < 3 × a codom (u1 k) \subset [:: p3; a[p1, p2] k].

    move⇒ /andP[k_gt0 k_ltb].

    rewrite {2}aE1 muln1 in k_ltb.

    rewrite ffunE !modn_small // !divn_small // inord_eq0 //.

    rewrite [in 3 × a.-1]aE1 /=.

    case: (k : nat) k_gt0 k_ltb ⇒ //= [] [|[|]] //= _ _.

      rewrite apegS apeg0.

      by have := sam1C; rewrite /pa aE1.

    by rewrite codom_subC.

  set x0S := sd u1.

  have P4 :
    (S_[3 × a] n.+1).*2 x0S + sp ↓[u ord0] 3 p1 +
                                 sp ↓[u (inord a)] 3 p2.

    apply: leq_trans (IH _ _ _ _ _ _ cH1) (leq_add (leq_add _ _) _);
        rewrite // 1?eq_sym //.

      by apply: leq_sumi _; rewrite ffunE /= inord_eq0 // aE1 muln1.

    by apply: leq_sumi _; rewrite ffunE /= mod3E /= div3E // aE1 muln1.

  have {}P4 := leq_trans P4 (leq_add (leq_add (leqnn _) (leq_sum_beta _ _))
                        (leqnn _)).

  set y0S := \sum_(_ < _) _ in P4; set y1S := sp _ _ _ in P4.

  have [b_gt1|b_le2] := leqP 2 b.

    pose u3 := [ffun i ↓[u (inord ((i : 'I_b.+1) + a))]].

    pose paS := a[p1, p3] a.+1.

    have cH6 (k : 'I_b.+1) :
        0 < k < b codom (u3 k) \subset [:: p2; a[pa, paS] k].

      move⇒ /andP[k_gt0 kLb].

      have kBound : 0 < k + a < l.+1.

        rewrite (leq_trans a_gt0) ?leq_addl //=.

        move: kLb; rewrite /b ltn_subRL addnC ⇒ /leq_trans→ //.

        by rewrite ltnW.

      rewrite ffunE codom_liftr //.

      have := @cH (inord (k + a)).

      rewrite /pa /paS apegS -apegD /= !inordK //; last first.

        by rewrite ltnW // ltnS; case/andP: kBound.

      by apply.

    have {cH6}P6 :
    (S_[b] n.+1).*2 sd u3 + sp (u3 ord0) b pa +
                               sp (u3 ord_max) b (a[pa, paS] b).

      apply: IH cH6 ⇒ //; try by rewrite /pa /paS // eq_sym.

      by rewrite /paS apegS apeg_eqC.

    set x1S := \sum_(_ _ < _) _.

    rewrite !ffunE (_ : sd u3 = x1S) in P6; last first.

      rewrite /x1S -[a]add0n big_addn -/b big_mkord.

      by apply: eq_bigri _; rewrite !ffunE !inordK ?ltnS // ltnW.

    rewrite add0n subnK // in P6.

    set y2S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6.

    have aLl : a l by apply: leq_trans aLa1 _.

    have y1Sy2SE : y1S + y2S (S_[1] n).*2 + α_[maxn 3 b] n.

      apply: sum_alpha_diffE ⇒ //; first by rewrite /pa eq_sym.

      apply/codom_liftr.

      have /cH : 0 < (inord a : 'I_l.+2) < l.+1 by rewrite inordK // a_gt0.

      by rewrite inordK // aE1 /=.

    pose u5 := [ffun i : 'I_3
                     if i == 0 :> nat then ↓[u (inord a1)]
                     else if i == 1 :> nat then sa1 else ta1].

    have cH7 (k : 'I_3) :
      0 < k < 2 codom (u5 k) \subset [:: p1; a[p2, p3] k].

      move⇒ /andP[k_gt0 k_lt2].

      rewrite !ffunE.

      by have ->/= : k = 1 :> nat by case: (k : nat) k_gt0 k_lt2 ⇒ // [] [|].

    have P7 :
      (S_[2] n.+1).*2
      (`d[↓[u (inord a1)], sa1]_smove + `d[sa1, ta1]_smove) +
         sp ↓[u (inord a1)] 2 p2 + sp ta1 2 p2.

      apply: (leq_trans (IH _ _ _ _ _ _ cH7)) ⇒ //.

        by rewrite eq_sym.

      repeat apply: leq_add; rewrite leq_eqVlt; apply/orP; left; apply/eqP.

      - by rewrite /sd !big_ord_recr big_ord0 !ffunE !inordK /=.

      - by apply: eq_bigri _; rewrite !ffunE.

      by apply: eq_bigri _; rewrite !ffunE.

    set x2S := (`d[_, _]_ _ + `d[_, _]_ _); rewrite -/x2S in P7.

    set y4S := sp _ _ _ in P7; set y5S := sp _ _ _ in P7.

    have y3Sy4SE : y3S + y4S (S_[1] n).*2 + α_[maxn b 2] n.

      apply: sum_alpha_diffE ⇒ //.

        by rewrite /paS apegS -apegD apeg_neq // eq_sym.

      apply: codom_liftr; rewrite codom_subC.

      have /cH : 0 < (inord a1 : 'I_l.+2) < l.+1.

        by rewrite inordK ?a1_gt0 // ltnS (leq_trans a1Ll).

      rewrite inordK ?ltnS ?(leq_trans a1Ll) //.

      by rewrite /paS apegS -apegD subnK.

    rewrite (maxn_idPl _) // in y3Sy4SE.

    have y5Sy7SE : y5S + y7S (S_[1] n).*2 + α_[maxn 2 (3 × c).-2] n.

      by apply: sum_alpha_diffE ⇒ //; first by rewrite /pa1 eq_sym.

    rewrite (maxn_idPr _) // in y5Sy7SE.

    rewrite -/y0S.

    move: P4 P6 P7 P8P4 P6 P7 P8.

    rewrite -(leq_add2r y1S); applyr P4.

    rewrite -(leq_add2r (y2S + y3S)); applyr P6.

    rewrite -(leq_add2r (y4S + y5S)); applyr P7.

    rewrite -(leq_add2r y7S); applyr P8.

    applyl y5Sy7SE; applyl y3Sy4SE; applyl y1Sy2SE.

    rewrite aE1 !muln1.

    have F1 := dsum_alphaL_S (3 × c).-2 n.

    rewrite [X in _ _ + X]mul2n -addnn -ltnS ![in X in _ X]addnA
            -![in X in _ X]addnS {2}F1 {F1}//.

    gsimpl.

    have F2 i k : 0 < i S_[i.-1] k.+1 S_[(3 ×i).-2] k + i.-1.

      movei_gt0; apply: leq_trans (dsum_alpha3l _ _) _.

      rewrite leq_add2r.

      apply: (increasingE (increasing_dsum_alphaL_l _)).

      by rewrite -{2}[i]prednK // mulnS addSn add2n /=.

    have F2n := F2 c n c_gt0.

    have F2n1 := F2 c n.+1 c_gt0.

    have F3 : c = c.-1.+1 by rewrite prednK.

    rewrite {}[in 2 × c]F3.

    gsimpl.

    applyr F2n; applyr F2n1; rewrite {F2}//.

    have l_gt1 : 1 < l.

      by rewrite -ltnS l1E aE1 add1n addSn ltnS (leq_trans b_gt1) // leq_addr.

    have F4 := SH l_gt1; applyl F4.

    have cB1_gt0 : 0 < c.-1 by rewrite -ltnS prednK.

    have F5 : S_[l.+1] n.+2 + S_[1] n.+2 S_[c.-1] n.+2 + S_[b.+3] n.+2.

      rewrite [X in _ X]addnC.

      rewrite (_ : l.+1 = 1 + c.-2 + b.+2); last first.

        by rewrite l1E aE1 !add1n -addSnnS !prednK // addnC.

      rewrite (_ : c.-1 = 1 + c.-2); last first.

         by rewrite add1n prednK // -ltnS prednK.

      by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).

    have F6 : S_[l] n.+1 + S_[1] n.+1 S_[c.-1] n.+1 + S_[b.+2] n.+1.

      rewrite [X in _ X]addnC.

      rewrite (_ : l = 1 + c.-2 + b.+1); last first.

        rewrite -[l]/(l.+1.-1) l1E aE1.

        by rewrite !add1n -addSnnS !prednK // addnC addnS.

      rewrite (_ : c.-1 = 1 + c.-2); last first.

         by rewrite add1n prednK // -ltnS prednK.

      by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).

    rewrite -(leq_add2r (S_[b.+2] n.+1)); applyr F6.

    rewrite -(leq_add2r (S_[b.+3] n.+2)); applyr F5; gsimpl.

    have [b_gt2|b_le3] := leqP 3 b.

      have F7 := dsum_alphaL_S b n; rewrite {}F7; gsimpl.

      have F8 : S_[b.+3] n.+2 S_[b.+2] n.+1 + (α_[1] n.+1).*2.

        by apply: dsum_alphaL_alpha.

      applyl F8.

      have F9 : S_[b.+1] n.+1 S_[b] n + (α_[1] n).*2.

        by apply: dsum_alphaL_alpha.

      rewrite -leq_double in F9.

      rewrite -(leq_add2r (4 × α_[1] n)); applyr F9.

      have F10 : S_[1] n.+1 + S_[b.+2] n.+1 S_[b.+1] n.+1 + S_[2] n.+1.

        rewrite addnC -[b.+2]/(1 + 1 + b).

        by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).

      rewrite -leq_double in F10; applyr F10.

      rewrite -2!ltnS [in X in _ X]mul2n -![in X in _ X]addSn -doubleS.

      have F11 := dsum_alpha3_S n.+1; rewrite -F11.

      have F12 := dsum_alphaL_S 1 n.+1; rewrite F12.

      have F13 := dsum_alphaL_S 1 n; rewrite !F13; gsimpl.

      by have F14 := alphaL_1_2 n; applyl F14; gsimpl.

    have bE2 : b = 2.

      by case: (b) b_gt1 b_le3 ⇒ // [] [|[|]].

    rewrite bE2.

    rewrite ![in X in _ X]mul2n -!addnn.

    have F1 := dsum_alphaL_S 2 n; rewrite {1}F1.

    have F2 := dsum_alphaL_S 3 n; rewrite {1}F2.

    have F3 : S_[5] n.+2 S_[4] n.+1 + (α_[1] n.+1).*2.

      by apply: dsum_alphaL_alpha.

    rewrite -[3 + 2]/5 -[2 + 2]/4; applyl F3.

    have F4 : S_[4] n.+1 S_[3] n + (α_[1] n).*2.

      by apply: dsum_alphaL_alpha.

    rewrite -leq_double in F4; applyl F4; gsimpl.

    rewrite -ltnS.

    have F5 := dsum_alpha3_S n.+1.

    rewrite -![in X in _ X]addSn -F5.

    have F6 := dsum_alpha3_S n.

    rewrite addnAC -!addnS -F6.

    rewrite -leq_double.

    have F7 := leq_dsum_alpha_2l_1 n.+1.

    have F8 := leq_dsum_alpha_2l_1 n.

    rewrite -[_ _]orFb -(leq_mul2l 3) in F7.

    applyr F7; applyr F8; gsimpl.

    have F9 := dsum_alphaL_S 1 n.+1.

    have F10 := dsum_alphaL_S 1 n.

    rewrite !(F9, F10); gsimpl.

    by have F11 := alphaL_1_2 n; applyl F11; gsimpl.

  have bE1 : b = 1.

    by case: (b) b_gt0 b_le2 ⇒ // [] [|].

  have a1E2 : a1 = 2.

    by move: bE1; rewrite /b aE1; case: (a1) ⇒ // [] [|[]].

  pose u3 :=
    [ffun i : 'I_4
    if i == 0 :> nat then ↓[u (inord a)] else
    if i == 1 :> nat then ↓[u (inord a1)] else
    if i == 2 :> nat then sa1 else ta1].

  set x1S := \sum_(_ _ < _) _.

  set d1 := `d[_, _]_ _ + `d[_, _]_ _.

  rewrite -/y0S.

  changer (a.*2 + x0S + c.*2 + x3S + y0S + y8S + (x1S + d1)).

  have → : x1S + d1 = \sum_(i < 3) `d[u3 (inord i), u3 (inord i.+1)]_smove.

    rewrite /x1S aE1 a1E2 big_nat1 /d1 !big_ord_recr big_ord0 /=.

    by rewrite !ffunE !inordK //= aE1 a1E2 add0n !addnA.

    have l_gt2 : 2 < l by rewrite -ltnS l1E aE1 bE1 !add1n.

  set x6S := \sum_(_ < 3) _.

  have cH6 (k : 'I_4) :
    0 < k < 3 codom (u3 k) \subset [:: pa1; a[pa1S, p2] k].

    move⇒ /andP[k_gt0 k_lt3].

    rewrite !ffunE eqn_leq leqNgt k_gt0 /=.

    case: eqP ⇒ [->/=|/eqP kD1].

      apply: codom_liftr; rewrite codom_subC.

      have /cH : 0 < (inord a1 : 'I_l.+2 ) < l.+1.

        by rewrite inordK a1E2 // (leq_trans l_gt2).

      by rewrite inordK // a1E2 (leq_trans l_gt2) // ltnW.

    have → : k = 2 :> nat.

      by case: (k : nat) k_gt0 k_lt3 kD1 ⇒ // [] [|[]].

    by have := sa1C; rewrite eqxx /pa1 /pa1S !(apegS, apeg0) codom_apeg.

  have P6 :
    (S_[3] n.+1).*2 x6S + sp (u3 ord0) 3 pa1S + sp (u3 ord_max) 3 p2.

    apply: IH cH6; rewrite /pa1S /pa1 //.

    by rewrite a1E2 eq_sym.

  rewrite !ffunE /= in P6.

  set y2S := sp _ _ _ in P6; set y3S := sp _ _ _ in P6.

  have y1Sy2SE : y1S + y2S (S_[1] n).*2 + α_[3] n.

    apply: sum_alpha_diffE ⇒ //; first by rewrite eq_sym /pa1S a1E2.

    have /H : 0 < (inord a : 'I_l.+2) < l.+1; first by rewrite inordK // aE1.

    by rewrite ffunE inordK // /pa1S /= aE1 a1E2.

  have lEc : l = c.+1 by rewrite -[l]/l.+1.-1 l1E aE1 bE1.

  rewrite lEc.

  have y3Sy7SE : y3S + y7S (S_[1] n).*2 + α_[maxn 3 (3 × c).-2] n.

    by apply: sum_alpha_diffE ⇒ //; first by rewrite /pa1 a1E2 eq_sym.

  rewrite (maxn_idPr _) in y3Sy7SE; last first.

    by rewrite -subn2 ltn_subRL ltnW // (leq_mul2l 3 2).

  move: P4 P6 P8P4 P6 P8.

  rewrite -(leq_add2r y1S); applyr P4.

  rewrite -(leq_add2r (y2S + y3S)); applyr P6.

  rewrite -(leq_add2r y7S); applyr P8.

  rewrite aE1 !muln1.

  applyl y1Sy2SE; applyl y3Sy7SE.

  rewrite ![in X in _ X]mul2n -!addnn.

  have F1 := dsum_alphaL_S 3 n; rewrite {1}F1.

  have F2 := dsum_alphaL_S (3 × c).-2 n; rewrite {1}F2; gsimpl.

  have F4 k : S_[c.-1] k.+1 S_[(3 ×c).-2] k + c.-1.

    apply: leq_trans (dsum_alpha3l _ _) _.

    rewrite leq_add2r.

    apply: (increasingE (increasing_dsum_alphaL_l _)).

    by rewrite -{2}[c]prednK // mulnS addSn add2n /=.

  have F4n := F4 n.

  have F4n1 := F4 n.+1.

  have F5 := prednK c_gt0.

  rewrite -{}[in 2 × c]F5.

  applyr F4n1; applyr F4n.

  have l_gt1 : 1 < l by rewrite lEc.

  have F6 : (S_[c.+2] n.+2).*2
             S_[c.+2] n.+2 + S_[c.+1] n.+1 + (α_[1] n.+1).*2.

    by have := (SH l_gt1); rewrite lEc.

  applyl F6.

  have F7 : S_[c.+2] n.+2 + S_[1] n.+2 S_[c.-1] n.+2 + S_[4] n.+2.

    rewrite (_ : c.+2 = 1 + 3 + c.-2); last first.

      by rewrite !addSn add0n !prednK ?addn2 // -ltnS prednK.

    rewrite {2}(_ : c.-1 = 1 + c.-2); last first.

      by rewrite add1n prednK // -ltnS prednK.

    by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).

  have F8 : S_[c.+1] n.+1 + S_[1] n.+1 S_[c.-1] n.+1 + S_[3] n.+1.

    rewrite (_ : c.+1 = 1 + 2 + c.-2); last first.

      by rewrite !addSn add0n !prednK ?addn2 // -ltnS prednK.

    rewrite {2}(_ : c.-1 = 1 + c.-2); last first.

      by rewrite add1n prednK // -ltnS prednK.

    by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).

  rewrite -(leq_add2r (S_[1] n.+2 + S_[1] n.+1)); applyl F7; applyl F8; gsimpl.

  have F9 : S_[4] n.+2 S_[3] n.+1 + (α_[1] n.+1).*2.

    by apply: dsum_alphaL_alpha.

  applyl F9.

  have F10 := dsum_alpha3_S n.

  have F11 := dsum_alpha3_S n.+1.

  gsimpl.

  rewrite -ltnS -![in X in _ X]addSn -{}F11.

  rewrite -ltnS -3![in X in _ X]addSn -[in X in _ X]addnS -{}F10.

  have F12 := dsum_alphaL_S 1 n.+1.

  have F13 := dsum_alphaL_S 1 n.

  rewrite F12 F13; gsimpl.

  have F14 := alphaL_1_2 n; rewrite -leq_double in F14.

  by applyl F14; gsimpl.

rewrite leqn0 ⇒ /eqP bE0.

have a1Ea : a1 = a by rewrite -(subnK aLa1) -/b bE0.

rewrite big_geq ?a1Ea // addn0.

have lEc : l = c by rewrite -[l]/(l.+1.-1) l1E aE1 bE0.

rewrite {1}lEc.

set d1 := `d[_, _]_ _ + `d[_, _]_ _.

set x0S := sd _; set y0S := \sum_(_ < _) _.

changer (a.*2 + c.*2 + x3S + y0S + y8S + (x0S + d1)).

pose u3 := [ffun i : 'I_6
  if i == 0 :> nat then ↓[u ord0] else
  if i == 1 :> nat then sam1 else
  if i == 2 :> nat then tam1 else
  if i == 3 :> nat then ↓[u (inord a1)] else
  if i == 4 :> nat then sa1 else
  ta1].

have → : x0S + d1 = sd u3.

  rewrite /x0S /d1 /sd.

  rewrite -(big_mkord xpredT (fun i`d[u1 (inord i), u1 (inord i.+1)]_ _)).

  rewrite {1}aE1 !(big_nat1, big_nat_recr) // !big_ord_recr big_ord0
          /= ?inordK //= !ffunE ?inordK ?a1Ea ?aE1 //=.

  by rewrite add0n !addnA inord_eq0.

have cH4 (k : 'I_6) :
    0 < k < 5 codom (u3 k) \subset [:: p3; a[p1, p2] k].

    case: k ⇒ [] [|[|[|[|[]]]]] //= iH _; rewrite !ffunE !(apegS, apeg0).

  - by have := sam1C; rewrite /pa aE1.

  - by rewrite codom_subC.

  - rewrite a1Ea aE1.

  - have /H : 0 < (inord 1 : 'I_l.+2) < l.+1 by rewrite !inordK.

    by rewrite ffunE inordK // codom_subC.

  by rewrite codom_subC.

have P4 :
  (S_[5] n.+1).*2 sd u3 + sp ↓[u ord0] 5 p1 + sp ta1 5 p2.

  apply: leq_trans (IH _ _ _ _ _ _ cH4) _ ⇒ //; first by rewrite eq_sym.

  by apply: leq_add; rewrite !ffunE.

have {}P4 := leq_trans P4
  (leq_add (leq_add (leqnn _) (leq_sum_beta _ _)) (leqnn _)).

rewrite -/y0S in P4; set y1S := sp _ _ _ in P4.

set x1S := sd _ in P4; rewrite -/x1S.

have y1Sy7SE : y1S + y7S (S_[1] n).*2 + α_[maxn 5 (3 × c).-2] n.

  apply: sum_alpha_diffE ⇒ //; first by rewrite /pa1 eq_sym.

move: P4 P8P4 P8.

rewrite -(leq_add2r y1S); applyr P4.

rewrite -(leq_add2r y7S); applyr P8.

rewrite aE1 muln1.

applyl y1Sy7SE.

have leq_S5 k : 2 × S_[1] k.+1 + S_[1] k.+2 3 × S_[5] k + 6.

  have F8 : S_[3] k + 2 × S_[6] k 3 × S_[5] k.

    rewrite -(leq_add2r (S_[4] k)).

    changel (S_[6] k + S_[3] k + (S_[6] k + S_[4] k)).

    changer (S_[4] k + S_[5] k + (S_[5] k + S_[5] k)).

    apply: leq_add.

      by apply: concaveEk1 3 2 1 (concave_dsum_alphaL_l _).

    by apply: concaveEk1 4 1 1 (concave_dsum_alphaL_l _).

  apply: leq_trans (leq_add F8 (leqnn _)).

  have F3k : S_[1] k.+1 S_[3] k + 1 by apply: dsum_alpha3l.

  have F3k1 : S_[2] k.+1 S_[6] k + 2 by apply: dsum_alpha3l.

  rewrite -leq_double in F3k1; applyr F3k1; applyr F3k; gsimpl.

  have F3k2 := leq_dsum_alpha_2l_1 k.+1.

  by applyr F3k2.

have [c_gt2|c_lt3] := leqP 3 c.

  rewrite (maxn_idPr _); last by rewrite -subn2 ltn_subRL (ltn_mul2l 3 2).

  have F1 k : S_[c.-1] k.+1 S_[(3 ×c).-2] k + c.-1.

    apply: leq_trans (dsum_alpha3l _ _) _.

    rewrite leq_add2r.

    apply: (increasingE (increasing_dsum_alphaL_l _)).

    by rewrite -{2}[c]prednK // mulnS addSn add2n /=.

  have F1n := F1 n.

  have F1n1 := F1 n.+1.

  have F2 := dsum_alphaL_S (3 × c).-2 n.

  rewrite [X in _ _ + X]mul2n -addnn {1}F2; gsimpl.

  have F3 : 2 × c = 2 + c.-1 + c.-1.

    by rewrite mul2n add2n prednK // addSnnS prednK // addnn.

  rewrite {}F3.

  applyr F1n; applyr F1n1.

  have F4 : S_[c.+1] n.+2 S_[c] n.+1 + (α_[1] n.+1).*2.

    by apply: dsum_alphaL_alpha.

  applyl F4.

  have F7n1 : S_[2] n.+2 + S_[c.+1] n.+2 S_[c.-1] n.+2 + S_[4] n.+2.

    rewrite addnC (_ : c.+1 = 2 + 2 + c.-2.-1); last first.

       by rewrite !addSn add0n !prednK // -ltnS prednK // -subn1 ltn_subRL //.

    rewrite {2}(_ : c.-1 = 2 + c.-1.-2); last first.

      by rewrite !addSn add0n !prednK // -?subn2 -?subn1 ltn_subRL.

    by apply: concaveEk1 (concave_dsum_alphaL_l n.+2).

  have F7n : S_[2] n.+1 + S_[c] n.+1 S_[c.-1] n.+1 + S_[3] n.+1.

    rewrite addnC {1}(_ : c = 2 + 1 + c.-1.-2); last first.

      by rewrite !addSn add0n !prednK // -2!ltnS !prednK // -ltnS prednK.

    rewrite {2}(_ : c.-1 = 2 + c.-1.-2); last first.

      by rewrite !addSn add0n !prednK // -?subn2 -?subn1 ltn_subRL.

    by apply: concaveEk1 (concave_dsum_alphaL_l n.+1).

  rewrite -(leq_add2l (S_[2] n.+2 + S_[2] n.+1)); applyl F7n1; applyl F7n.

  gsimpl.

  have F8 := leq_S5 n.+1.

  have F9 : S_[4] n.+2 S_[3] n.+1 + (α_[1] n.+1).*2.

    by apply: dsum_alphaL_alpha.

  applyl F9.

  rewrite -[_ _](leq_mul2l 3).

  rewrite -leq_double in F8; applyr F8.

  have F10 := dsum_alpha3_S n.+1.

  rewrite -(leq_add2r 6).

  changel (12 × (α_[1] n.+1) + 6 × (S_[1] n) + 6 × (S_[3] n.+1).+1).

  rewrite -F10.

  rewrite -leq_double.

  have F11 := leq_dsum_alpha_2l_1 n.+2.

  rewrite -[_ _](leq_mul2l 3) in F11.

  have F12 := leq_dsum_alpha_2l_1 n.+1.

  rewrite -[_ _](leq_mul2l 3) in F12.

  applyr F11; applyr F12; gsimpl.

  have F13 := dsum_alphaL_S 1 n.+2.

  have F14 := dsum_alphaL_S 1 n.+1.

  have F15 := dsum_alphaL_S 1 n.

  rewrite !(F13, F14, F15); gsimpl.

  have F16 := increasing_alphaL 1 n.+1.

  rewrite -[15]/(7 + 8) mulnDl [X in _ X]addnAC [X in _ X]addnC leq_add //.

    by rewrite leq_mul2l.

  case: (n) ⇒ [|[|[|[|n1]]]]; rewrite ?alpha_small //.

  have F17 : 3 × α_[1] n1.+1.+4 4 × α_[1] n1.+4.

    by rewrite alpha_4_3.

  rewrite -[_ _]orFb -(leq_mul2l 8) mulnA in F17.

  rewrite -[_ _](leq_mul2l 3) mulnA.

  by apply: leq_trans F17 _; gsimpl.

have cE2 : c = 2 by case: (c) c_gt1 c_lt3 ⇒ [|[|[|]]].

rewrite cE2 (maxn_idPl _) // add1n -[2 × 2]/4 -[(3 × 2).-2]/4 -[2 + 4]/6.

rewrite [in X in _ X]mul2n -addnn.

have F1 := dsum_alphaL_S 5 n; rewrite {1}F1.

have F2 := dsum_alpha3_S n.+2.

rewrite -2!ltnS mul2n -![in X in X _]addSn -doubleS -{}F2.

have F3 := leq_S5 n.

have F4 := leq_S5 n.+1.

rewrite -[_ _](leq_mul2l 3); gsimpl.

applyr F3; applyr F4.

have F5 := leq_S4 n.+1; applyr F5.

have F6 := dsum_alphaL_S 1 n.+2.

have F7 := dsum_alphaL_S 1 n.+1.

have F8 := dsum_alphaL_S 1 n.

rewrite !(F6, F7, F8); gsimpl.

have F10 := alphaL_1_2 n.+1.

rewrite -[_ _]orFb -(leq_mul2l 4) in F10.

applyl F10; gsimpl.

case: (n) ⇒ [|[|[|[|n1]]]]; rewrite ?alpha_small //.

have F9 : 3 × α_[1] n1.+1.+4 4 × α_[1] n1.+4.

  by rewrite alpha_4_3.

rewrite -[_ _]orFb -(leq_mul2l 4) in F9.

rewrite -[_ _](leq_mul2l 3).

by rewrite add1n; applyl F9; gsimpl.

Qed.


End Case3.


Lemma main p1 p2 p3 n l (u : {ffun 'I_l.+1 configuration 4 n}) :
   p1 != p2 p1 != p3 p2 != p3
   p1 != p0 p2 != p0 p3 != p0
  ( k : 'I_l.+1, 0 < k < l
                       codom (u k) \subset [:: p2; a[p1, p3] k])
  (S_[l] n).*2 \sum_(i < l) `d[u (inord i), u (inord i.+1)]_smove +
                    \sum_(k < n) (u ord0 k != p1) × β_[n, l] k +
                    \sum_(k < n) (u ord_max k != a[p1, p3] l) × β_[n, l] k.

Proof.

elim: n l p1 p2 p3 u ⇒ [|[|n] IH] l p1 p2 p3
                u p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 cH.

- by rewrite /dsum_alphaL /conv /= dsum_alpha_0 muln0.

- rewrite /dsum_alphaL /conv /= dsum_alpha_1 dsum_alpha_0
          muln0 addn0 add0n muln1.

  rewrite [X in _ _ + X + _]big_ord_recl big_ord0 /= addn0.

  rewrite [X in _ _ + X]big_ord_recl big_ord0 /= addn0.

  have d0fE (c1 c2 : configuration 4 1) :
    c1 != `c[p0] c2 != `c[p0] `d[c1, c2]_smove = (c1 != c2).*2.

    movec1Dp0 c2Dp0.

    case: (gpath_connect (shanoi_connect c1 c2))
              ⇒ [] [/gpath_dist H |a [|b p]].

    - by rewrite H; move/eqP: H; rewrite gdist_eq0 ⇒ →.

    - case/gpathP; rewrite /= andbT ⇒ /moveP[z].

      rewrite [z]disk1_all ⇒ [] [zH _ _ _] aE.

      case/andP: zH_; rewrite aE.

      move: c1Dp0 c2Dp0; rewrite !configuration1_eq !Ival_eq /= !ffunE /=.

      by do 2 case: val.

    move⇒ /gpath_dist; case: eqP ⇒ [<-|/eqP c1Dc2]; first by rewrite gdist0.

    moveH; apply/eqP; rewrite eqn_leq {2}H /= andbT.

    have pH : path smove c1 [::`c[p0]; c2].

      rewrite /=; apply/and3P; split ⇒ //.

        apply/moveP; ord0; split ⇒ //=.

        - rewrite !ffunE; apply/andP; split; last by rewrite muln0.

          by move: c1Dp0; rewrite configuration1_eq ffunE.

        - by movei; rewrite [i]disk1_all.

        - by apply/on_topPj; rewrite [j]disk1_all.

        by apply/on_topPj; rewrite [j]disk1_all.

      apply/moveP; ord0; split ⇒ //=.

      - rewrite !ffunE; apply/andP; split⇒ //.

        by move: c2Dp0; rewrite configuration1_eq ffunE eq_sym.

      - by movei; rewrite [i]disk1_all.

      - by apply/on_topPj; rewrite [j]disk1_all.

      by apply/on_topPj; rewrite [j]disk1_all.

    rewrite -[1.*2]/(size [:: `c[p0]; c2]).

    by apply: gdist_path_le pH _.

  case: l u cH ⇒ [|l] u cH; first by rewrite (minn_idPr _).

  case: l u cH ⇒ [|l] u cH.

    rewrite (minn_idPr _) //.

    rewrite big_ord_recl big_ord0 addn0.

    rewrite inord_eq0 // (_ : inord 1 = ord_max); last first.

      by apply/val_eqP; rewrite /= inordK.

    rewrite /beta !(apegS, apeg0) /= alphaL1E -[_ 0]/1;
        do 2 case: eqP; rewrite /= ?addn0;
        try by move⇒ *; rewrite leq_addl.

    moveu1E u0E.

    rewrite d0fE //.

    - by rewrite configuration1_eq u1E u0E p1Dp3.

    - by rewrite configuration1_eq ffunE u0E.

    by rewrite configuration1_eq ffunE u1E.

  rewrite (minn_idPl _) // -[_.*2]/4.

  rewrite big_ord_recl big_ord_recr /=.

  rewrite -!addnA addnC -!addnA (leq_trans _ (leq_addl _ _)) //.

  rewrite !apegS /beta /= alphaL_0 (minn_idPl _) /bump /= ?add1n //.

  rewrite addnCA addnC !addnA -addnA -[4]/(2 + 2).

  apply: leq_add.

    case: eqP ⇒ /= [umE|umD]; last by rewrite leq_addl.

    rewrite addn0 d0fE.

    - case: eqP ⇒ // H.

      have /cH : 0 < (inord l.+1 : 'I_l.+3) < l.+2 by rewrite inordK /=.

      move⇒ /subsetP/(_ _ (codom_f _ sdisk)).

      rewrite H (_ : inord l.+2 = ord_max).

        rewrite umE inordK // apegS //= !inE.

        rewrite (apeg_eqC _ _ _) // (negPf (apeg_neq _ _ _)) //=.

          by rewrite (negPf p1Dp3).

        by rewrite eq_sym.

      by apply/val_eqP; rewrite /= inordK.

    - rewrite configuration1_eq ffunE.

      case: (_ =P _) ⇒ // H.

      have /cH : 0 < (inord l.+1 : 'I_l.+3) < l.+2 by rewrite inordK /=.

      move⇒ /subsetP/(_ _ (codom_f _ sdisk)).

      by rewrite H !inE eq_sym (negPf p2Dp0) /= eq_sym (negPf (apeg_neq _ _ _)).

    rewrite configuration1_eq ffunE.

    rewrite (_ : inord l.+2 = ord_max).

      by rewrite umE apeg_neq.

    by apply/val_eqP; rewrite /= inordK.

  case: eqP ⇒ /= [u0E|u0D]; last by rewrite leq_addl.

  rewrite addn0 d0fE.

  - case: eqP ⇒ // H.

    have /cH : 0 < (inord 1 : 'I_l.+3) < l.+2 by rewrite inordK /=.

    move⇒ /subsetP/(_ _ (codom_f _ sdisk)).

    rewrite -H inord_eq0 // u0E inordK //= !(apegS, apeg0).

    by rewrite !inE (negPf p1Dp2) (negPf p1Dp3).

  - by rewrite configuration1_eq ffunE inord_eq0 // u0E.

  rewrite configuration1_eq ffunE.

  case: eqP ⇒ // H.

  have /cH : 0 < (inord 1 : 'I_l.+3) < l.+2 by rewrite inordK /=.

  move⇒ /subsetP/(_ _ (codom_f _ sdisk)).

  by rewrite H !inE eq_sym (negPf p2Dp0) /= eq_sym (negPf (apeg_neq _ _ _)).

case: l u cH ⇒ [|l] u cH; first by rewrite S0E.

rewrite apegS.

pose u' : {ffun 'I_l.+2 configuration 4 n.+1} :=
     [ffun i : 'I_l.+2 ↓[u i]].

have H (k : 'I_l.+2) :
  0 < k < l.+1 codom (u' k) \subset [:: p2; a[p1, p3] k].

  by movek1; rewrite ffunE; apply/codom_liftr/cH.

pose K := (u ord0 ord_max != p1) +
          (u ord_max ord_max != a[p3, p1] l).

have [HK|] := boolP ((K == 2) || ((K == 1) && (l == 0))).

  rewrite dsum_alphaL_S doubleD.

  have IH' := IH _ p1 p2 p3 u'
              p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 H.

  rewrite apegS in IH'.

  rewrite ![\sum_(_ < _.+2) _]big_ord_recr /=.

  set u1 := \sum_ (_ < _) _; set u2 := \sum_ (_ < _) _; set u3 := \sum_ (_ < _) _.

  rewrite -!addnA [_ + (u3 + _)]addnCA 2!addnA.

  apply: leq_add.

    apply: leq_trans IH' _.

    apply: leq_add; last first.

      apply: leq_sumi _.

      apply: leq_mul.

        rewrite leq_eqVlt; apply/orP; left; apply/eqP.

        by rewrite !ffunE; congr (u _ _ != _); apply/val_eqP.

      rewrite {2}/beta eqn_leq [_ i]leqNgt ltn_ord !andbF /=.

    apply: geq_beta.

    apply: leq_add; last first.

      apply: leq_sumi _.

      apply: leq_mul.

        rewrite leq_eqVlt; apply/orP; left; apply/eqP.

        by rewrite !ffunE; congr (u _ _ != _); apply/val_eqP.

      rewrite {2}/beta eqn_leq [_ i]leqNgt ltn_ord !andbF /=.

      apply: geq_beta.

    apply: leq_sumi _.

    rewrite !ffunE.

    by apply/gdist_cunlift/shanoi_connect.

  rewrite -mulnDl -/K.

  case/orP: HK ⇒ [/eqP->|/andP[/eqP→ /eqP->]].

    by rewrite mul2n leq_double leq_beta.

  by rewrite mul1n /beta /= /alphaL /delta !S1E.

rewrite negb_or negb_and.

have: K 2 by rewrite /K; do 2 case: (_ != _).

case: ltngtP; rewrite // ltnS.

case: ltngtP ⇒ //= KE _ _ l_gt0; last first.

  move: KE; rewrite /K.

  (case: eqP ⇒ [KH1|/eqP KH1] /=; case: eqP) ⇒ // [/eqP KH2|KH2] _.

    by apply: (@case1 _ IH) cH KH1 KH2 l_gt0.

  pose u1 : {ffun 'I_l.+2 configuration 4 n.+2} :=
     [ffun i : 'I_l.+2 u (inord (l.+1 - i))].

  have → : \sum_(i < l.+1) `d[u (inord i), u (inord i.+1)]_smove =
            \sum_(i < l.+1) `d[u1 (inord i), u1 (inord i.+1)]_smove.

    have F : injective (fun i : 'I_l.+1 ⇒ (inord (l - i) : 'I_l.+1)).

      movei j /val_eqP.

      have lBiLl (i1 : 'I_l.+1) : l - i1 < l.+1.

        by rewrite ltn_subLR ?leq_addl // -ltnS.

      rewrite /= !inordK // ⇒ /eqP liE; apply/val_eqP ⇒ /=.

      rewrite -(subKn (_ : i l)); last by rewrite -ltnS.

      by rewrite liE subKn // -ltnS.

    rewrite (reindex_inj F) /=.

    apply: eq_bigri _; rewrite !ffunE.

    have iLl2 : i < l.+2 by apply: leq_trans (ltn_ord _) _.

    have lBiLl : l - i < l.+1 by rewrite ltn_subLR ?leq_addl // -ltnS.

    have iLl : i l by rewrite -ltnS.

    rewrite gdistC; last by apply/move_sym/ssym.

    congr (`d[u _,u _]_smove).

      by apply/val_eqP; rewrite /= !inordK ?subSn.

    by apply/val_eqP; rewrite /= !inordK // ?subSS ltnS // ltnW.

  pose p1' := a[p3, p1] l.

  pose p3' := a[p1, p3] l.

  have → : \sum_(k < n.+2) (u ord0 k != p1) × β_[n.+2, l.+1] k =
            \sum_(k < n.+2) (u1 ord_max k != a[p1', p3'] l.+1) ×
                            β_[n.+2, l.+1] k.

    apply: eq_bigri _; congr (_ × _).

    rewrite ffunE subnn.

    by rewrite inord_eq0 // -apegD addSn addnn apegS apeg_double.

  have → : \sum_(k < n.+2)
              (u ord_max k != a[p3, p1] l) × β_[n.+2, l.+1] k =
            \sum_(k < n.+2) (u1 ord0 k != p1') × β_[n.+2, l.+1] k.

    apply: eq_bigri _; congr (_ × _).

    rewrite ffunE subn0.

    suff → : inord l.+1 = ord_max :> 'I_l.+2 by [].

    by apply/val_eqP; rewrite /= inordK.

  have cH1 (k : 'I_l.+2) :
     0 < k < l.+1 codom (u1 k) \subset [:: p2; a[p1', p3'] k].

    move⇒ /andP[kH1 kH2]; rewrite ffunE.

    have F1 : k l.+1 by apply: ltnW.

    have F2 : l.+1 - k < l.+2.

      by rewrite ltn_subLR // addnS ltnS leq_addl.

    have → : a[p1', p3'] k = a[p1, p3] (inord (l.+1 - k) : 'I_l.+2).

      rewrite -apegD inordK // [RHS]apegO oddB //.

      by rewrite -oddD -apegO addSn apegS addnC.

    apply: cH; rewrite inordK // subn_gt0 // ltn_subLR // kH2 //=.

    by rewrite addnS ltnS -{1}[l.+1]add1n leq_add2r.

  rewrite -addnA [X in _ _ + X]addnC addnA apegS.

  apply: (@case1 _ IH) cH1 _ _ _ ⇒ //.

  - by rewrite apeg_neq // eq_sym.

  - by rewrite apeg_eqC // eq_sym.

  - by rewrite eq_sym apeg_neq // eq_sym.

  - by rewrite apeg_neq // eq_sym.

  - by rewrite apeg_neq // eq_sym.

  - rewrite ffunE subn0.

    suff → : inord l.+1 = ord_max :> 'I_l.+2 by [].

    by apply/val_eqP; rewrite /= inordK.

  by rewrite ffunE subnn inord_eq0 // -apegD addnn apeg_double.

move: KE; rewrite /K; do 2 case: eqP ⇒ //=.

moveuME u0E _.

by apply: (case3 IH _ _ _ _ _ _ cH).

Qed.


Lemma main_cor p1 p2 n :
  p1 != p0 p2 != p0 p1 != p2
  (S_[1] n).*2 `d[`c[p1, n],`c[p2, n]]_smove.

Proof.

movep1Dp0 p2Dp0 p1Dp2.

rewrite eq_sym in p2Dp0.

have [p3 [[p3Dp2 p3Dp0 p3Dp1] _]] := peg4comp3 p1Dp0 p1Dp2 p2Dp0.

rewrite eq_sym in p2Dp0.

pose u := [ffun i : 'I_2 if i == 0 :> nat then
                             `c[p1, n] else `c[p2, n]].

suff :
  (S_[1] n).*2
  \sum_(i < 1) `d[u (inord i), u (inord i.+1)]_smove +
  \sum_(k < n) (u ord0 k != p1) × β_[n, 1] k +
  \sum_(k < n) (u ord_max k != p2) × β_[n, 1] k.

  rewrite big_ord_recr big_ord0 !ffunE /= inord_eq0 //= add0n.

  rewrite inordK //=.

  rewrite (eq_bigr (fun i : 'I_n ⇒ 0)) ⇒ [|i _]; last first.

    by rewrite !ffunE eqxx.

  rewrite -(big_mkord xpredT (fun 0)) sum_nat_const_nat muln0.

  rewrite (eq_bigr (fun i : 'I_n ⇒ 0)) ⇒ [|i _]; last first.

    by rewrite !ffunE eqxx.

  rewrite -(big_mkord xpredT (fun 0)) sum_nat_const_nat muln0.

  by rewrite !addn0.

apply: (@main p1 p3 p2) ⇒ //.

  by rewrite eq_sym.

by case⇒ [] [].

Qed.


Lemma gdist_shanoi4 (n : nat) (p1 p2 : peg 4) :
  p1 != p2 p1 != p0 p2 != p0
  `d[`c[p1, n], `c[p2, n]]_smove = (S_[1] n).*2.

Proof.

movep1Dp2 p1Dp0 p2Dp0; apply/eqP; rewrite eqn_leq.

by rewrite leq_shanoi4 // main_cor.

Qed.


End sHanoi4.